Publikationen zum Fachbereich LoLA

Publikationen in Zeitschriften und Büchern

• Karsten Schmidt. Distributed Verification with LoLA. Fundamenta Informaticae, 54(2-3): 253-262, 2003.

  Abstract: We report work in progress on a distributed version of explicit state space generation in the Petri net verification tool LoLA. We propose a data structure where all available memory of all involved workstations can be fully exploited, and load balancing actions are possible at any time while the verification is running. It is even possible to extend the set of involved workstations while a verification is running.

  

• Karsten Schmidt. Flexible net Inscriptions with LoLA. Petri Net Newsletter, 59: 30-44, 2000.

Konferenzbeiträge und Beiträge auf Workshops

• Sebastian Hinz, Karsten Schmidt, and Christian Stahl. Transforming BPEL to Petri Nets. In Wil M. P. van der Aalst, B. Benatallah, F. Casati, and F. Curbera, editors, Proceedings of the Third International Conference on Business Process Management (BPM 2005), volume 3649 of Lecture Notes in Computer Science, Nancy, France, pages 220-235, September 2005. Springer-Verlag.

  Abstract: We present a Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics covers the standard behaviour of BPEL as well as the exceptional behaviour (e.g. faults, events, compensation). The semantics is implemented as a parser that translates BPEL specifications into the input language of the Petri net model checking tool LoLA. We demonstrate that the semantics is well suited for computer aided verification purposes.

  

• Christian Stahl, Wolfgang Reisig, and Milos Krstic. Hazard Detection in a GALS Wrapper: A Case Study. In Jörg Desel and Y. Watanabe, editors, Proceedings of the Fifth International Conference on Application of Concurrency to System Design (ACSD'05), St. Malo, France, pages 234-243, June 2005. IEEE Computer Society.

  Abstract: An asynchronous wrapper of a fabricated GALS system is analyzed for hazards. For this purpose a Petri net based modelling approach of this GALS wrapper is presented. In our model the question whether a hazard can occur in a gate is reduced to a model checking problem: the reachability of a particular marking in the Petri net. In order to alleviate state space explosion two techniques to reduce the model's state space are presented. By use of these techniques we detected several potential hazards and a deadlock in the wrapper.

  

• Karsten Schmidt and Christian Stahl. A Petri net semantic for BPEL4WS - validation and application. In Ekkart Kindler, editor, Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN'04), pages 1-6, October 2004. Universität Paderborn.

  Abstract: We translated a small business process into a recently defined Petri net semantic. Then we used the tool LoLA for validating the semantic as well as for proving relevant properties of the particular process.

  

• Karsten Schmidt. LoLA: A Low Level Analyser. In Mogens Nielsen and Dan Simpson, editors, Application and Theory of Petri Nets, 21st International Conference (ICATPN 2000), volume 1825 of Lecture Notes in Computer Science, pages 465-474, June 2000. Springer-Verlag.

  Abstract: With LoLA, we put recently developed state space oriented algorithms to other tool developers disposal. Providing a simple interface was a major design goal such that it is as easy as possible to integrate LoLA into tools of different application domains. LoLA supports place/transition nets. Implemented verification techniques cover standard properties (liveness, reversibility, boundedness, reachability, dead transitions, deadlocks, home states) as well as satisfiability of state predicates and CTL model checking. For satisfiability, both exhaustive search and heuristically goal oriented system execution are supported. For state space reduction, LoLA features symmetries, stubborn sets, and coverability graphs.

  

• Karsten Schmidt. LoLA wird Pfadfinder. In Workshop Algorithmen und Werkzeuge für Petrinetze, Frankfurt, pages 48-53, 1999.

  Abstract: LoLA ist ein erreichbarkeitsgraphbasiertes Werkzeug für Stellen/Transitions-Netze. Hier geht es um LoLAs Fähigkeit, erreichbare Zustände mit vorgegebenen Eigenschaften zu suchen und im Erfolgsfall einen solchen Zustand mit einem Weg von der Anfangsmarkierung dorthin anzugeben. Die Besonderheit besteht darin, daß während der Suche nur zwei Zustände gespeichert werden: der Anfangszustand und der aktuelle Zustand. Anstatt also den Zustandsraum systematisch zu durchmustern (und dabei meist am Speicherende zu scheitern), navigiert LoLA ohne Kenntnis der schon betretenen Zustände durch den Erreichbarkeitsgraph. Daß sie trotzdem ihre Aufgabe erfolgreich löst, liegt an ihren spezifischen Fähigkeiten: Schnelligkeit, Bescheidenheit, Zielstrebigkeit, Neugier und Ausdauer.

  

Technische Berichte

• Dirk Fahland. Translating UML2 Activity Diagrams Petri Nets for analyzing IBM WebSphere Business Modeler process models. Informatik-Berichte 226, Humboldt-Universität zu Berlin, 2008.

  Abstract: We present a formal semantics for a variant of UML2 Activity Diagrams that is used in the IBM WebSphere Business Modeler for modeling business processes. Business process models created in the IBM WebSphere Business Modeler or with other UML2 modeling tools often constitutes one of the key specification artifacts for building an information system that implements or supports the specified processes. As UML2 Activity Diagrams lack a universally agreed semantics, the step from specification to implementation usually faces a semantical impedance caused by different interpretation of the same diagram. A well-defined formal semantics for the specification language determines the interpretation of a diagram and allows for reasoning about as well as validating and verifying a given specification on common (formal) grounds. We adapt approaches for formalizing semantics of UML2 Activity Diagrams and apply them to the core features of the IBM WebSphere Business Modeler language for purpose of formal verification. We provide a parameterized Petri net pattern for each language concepts. A diagram is translated by instantiating a pattern for each use of a concept; merging the resulting Petri net fragments according to the structure of the original diagram yields a Petri net that specifies the behavioral semantics of the diagram. The resulting Petri net can be verified for control-flow errors using the model checker LoLA. The semantics has been implemented in a tool that is available at http://www.service-technology.org/uml2owfn/.

  

• Christian Stahl, Wolfgang Reisig, and Milos Krstic. Hazard Detection in a GALS Wrapper: a Case study. Informatik-Berichte 184, Humboldt-Universität zu Berlin, February 2005.

  Abstract: An asynchronous wrapper of a fabricated GALS system is analyzed for hazards. For this purpose a Petri net based modelling approach of this GALS wrapper is presented. In our model the question whether a hazard can occur in a gate is reduced to a model checking problem: the reachability of a particular marking in the Petri net. In order to alleviate state space explosion three techniques to reduce the model?s state space are presented. By use of these techniques we detected several potential hazards in the wrapper.

  

zurück zur Übersicht