Publications
-
Matthias Kuntz, Stefan Leue, Christoph Scheben, Wei Wei, Sen Yang: Heuristic Search for Unbounded Executions, Technical Report soft-09-02, Chair for Software Engineering, University of Konstanz, 2009.
Download: [PDF]Abstract: 
We present a heuristic search based approach to finding un- bounded executions in software models that can be described using Com- municating Finite State Machines (CFSMs). This improves the unbound- edness test devised by Jeron and Jard in case certain knowledge about potential sources of unboundedness is available. Such knowledge can be obtained from a boundedness analysis that we designed in precursory work. We evaluate the effectiveness of several different heuristics and search strategies. To show the feasibility of our approach, we compare the performance of the heuristic search algorithms with that of uninformed search algorithms in detecting unbounded executions for a number of case studies. We discuss the applicability of our approach to high level modeling languages for concurrent systems such as Promela. -
Husain Aljazzar and Stefan Leue: Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking, IEEE Transactions on Software Engineering, IEEE computer Society Digital Library, IEEE Computer Society, 2009.
Download: [PDF]Abstract: Current stochastic model checkers do not make counterexamples for property violations readily available. In this paper we apply directed explicit state space search to discrete- and continuous-time Markov chains in order to compute counterexamples for the violation of PCTL or CSL properties. Directed explicit state space search algorithms explore the state space on-the-fly which makes our method very efficient and highly scalable. They can also be guided using heuristics which usually improve the performance of the method. Counterexamples provided by our method have two important properties. First, they include those traces which contribute the most amount of probability to the property violation. Hence, they show the most probable offending execution scenarios of the system. Second, the obtained counterexamples tend to be small. Hence, they can be effectively analyzed by a human user. Both properties make the counterexamples obtained by our method very useful for debugging purposes. We implemented our method based on the stochastic model checker PRISM and applied it to a number of case studies in order to illustrate its applicability. -
Bahareh Badban, Stefan Leue, Jan-Georg Smaus: Automated Predicate Abstraction for Real-Time Models, Accepted for publication in INFINITY 2009, 11th International Workshop on Verification of Infinite-State Systems, 2009.
Abstract: We present a technique designed to automatically compute predicate abstractions for dense real-timed models represented as networks of timed automata. We use the CIPM algorithm in our previous work which computes new invariants for timed automata control locations and prunes the model, to compute a predicate abstraction of the model. We do so by taking information regarding control locations and their newly computed invariants into account. We also discuss a prototype implementation of our technique. -
Bahareh Badban, Stefan Leue, Jan-Georg Smaus: Automated Invariant Generation for the Verification of Real-Time Systems, in the International Workshop on Invariant Generation (WING), 2009.
Abstract: We present a technique designed to automatically compute predicate abstractions for dense real-timed models represented as networks of timed automata. We first introduce the CIPM algorithm which computes new invariants for timed automata control locations taking their originally defined invariants as well as the constraints imposed by incoming state transitions into account. CIPM also prunes transitions that can never be taken from the automaton. We then compute a predicate abstraction taking information regarding control locations and their newly computed invariants into account. We finally discuss a prototype implementation of our technique. -
Bahareh Badban: A Term Rewriting Technique for Decision Graphs, in the International Workshop on Computing with Terms and Graphs (TERMGRAPH), 2009.
Download: [PDF]Abstract: We provide an automatic verification for a fragment of FOL quantifier-free logic with zero, successor and equality. We use BDD representation of such formulas and to verify them, we first introduce a (complete) term rewrite system to generate an equivalent Ordered (0, S,=)-BDD from any given (0, S,=)-BDD. Having the ordered representation of the BDDs, one can verify the original formula in constant time. Then, to have this transformation automatically, we provide an algorithm which will do the whole process. -
Stefan Edelkamp, Viktor Schuppan, Dragan Bosnacki, Anton Wijs, Ansgar Fehnker and Husain Aljazzar: Survey on Directed Model Checking, Volume 5348, Pages 65-89, Model Checking and Artificial Intelligence, 5th International Workshop, MoChArt '08. Revised Selected and Invited Papers, Lecture Notes in Computer Science, Springer Verlag, 2009.
Download: [PDF]Abstract: This article surveys and gives historical accounts to the algorithmic essentials of /directed model checking/, a promising bug-hunting technique to mitigate the state explosion problem. In the enumeration process, successor selection is prioritized. We discuss existing guidance and methods to automatically generate them by exploiting system abstractions. We extend the algorithms to feature partial-order reduction and show how liveness problems can be adapted by lifting the search space. For deterministic, finite domains we instantiate the algorithms to directed symbolic, external and distributed search. For real-time domains we discuss the adaption of the algorithms to timed automata and for probabilistic domains we show the application to counterexample generation. Last but not least, we explain how directed model checking helps to accelerate finding solutions to scheduling problems. -
Husain Aljazzar and Stefan Leue: Generation of Counterexamples for Model Checking of Markov Decision Processes, Proceedings of 6th International Conference on the Quantitative Evaluation of SysTems (QEST '09), IEEE Computer Society Press, 2009.
Abstract: The practical usefulness of a model checker as a debugging tool relies on its ability to provide diagnostic information, sometimes also referred to as a counterexample. Current stochastic model checkers do not provide such diagnostic information. In this paper we address this problem for Markov Decision Processes. First, we define the notion of counterexamples in this context. Then, we discuss three methods to generate informative counterexamples which are helpful in system debugging. We point out the advantages and drawbacks of each method. We also experimentally compare all three methods. Our experiments demonstrate the conditions under which each method is appropriate to be used. -
H. Aljazzar, M. Fischer, L. Grunske, M. Kuntz, F. Leitner-Fischer, S. Leue: Safety Analysis of an Airbag System using Probabilistic FMEA and Probabilistic Counter Examples, Proceedings of 6th International Conference on the Quantitative Evaluation of SysTems (QEST '09), IEEE Computer Society Press, 2009.
Download: [PDF]Abstract: Failure mode and effects analysis (FMEA) is a technique to reason about possible system hazards that result from system or system component failures. Traditionally, FMEA does not take the probabilities with which these failures may occur into account. Recently, this shortcoming was addressed by integrating stochastic model checking techniques into the FMEA process. A further improvement is the integration of techniques for the generation of counterexamples for stochastic models, which we propose in this paper. Counterexamples facilitate the redesign of a potentially unsafe system by providing information which components contribute most to the failure of the entire system. The usefulness of this novel approach to the FMEA process is illustrated by applying it to the case study of an airbag system provided by our industrial partner, the TRW Automotive GmbH. -
Christian Dax, Felix Klaedtke and Stefan Leue: Specification Languages for Stutter-Invariant Regular Properties, To appear in: Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Lecture Notes in Computer Science, Springer Verlag, 2009.
Abstract: Not available. -
Husain Aljazzar, Manuel Fischer, Lars Grunske, Matthias Kuntz, Florian Leitner-Fischer, Stefan Leue: Safety Analysis of an Airbag System using Probabilistic FMEA and Probabilistic Counter Examples, Technical Report soft-09-01, Chair for Software Engineering, University of Konstanz, 2009.
Download: [PDF]Abstract: Failure mode and effects analysis (FMEA) is a technique to reason about possible system hazards that result from system or system component failures. Traditionally, FMEA does not take the probabilities with which these failures may occur into account. Recently, this shortcoming was addressed by integrating stochastic model checking techniques into the FMEA process. A further improvement is the integration of techniques for the generation of counter examples for stochastic models, which we propose in this paper. Counter examples facilitate the redesign of a potentially unsafe system by providing information which components contribute most to the failure of the entire system. The usefulness of this novel approach to the FMEA process is illustrated by applying it to the case study of an airbag system provided by our industrial partner, the TRWAutomotive GmbH. -
Dragan Bosnacki, Stefan Leue and Alberto Lluch Lafuente: Partial-order reduction for general state exploring algorithms , Volume 11, Pages 39-51, International Journal on Software Tools for Technology Transfer (STTT), Springer Berlin / Heidelberg, DOI: 10.1007/s10009-008-0093-y, 2009.
Download: [PDF]Abstract: Partial-order reduction is one of the main techniques used to tackle the combinatorial state explosion problem occurring in explicit-state model checking of concurrent systems. The reduction is performed by exploiting the independence of concurrently executed events, which allows portions of the state space to be pruned. An important condition for the soundness of partial-order-based reduction algorithms is a condition that prevents indefinite ignoring of actions when pruning the state space. This condition is commonly known as the cycle proviso. In this paper, we present a new version of this proviso, which is applicable to a general search algorithm skeleton that we refer to as the general state exploring algorithm (GSEA). GSEA maintains a set of open states from which states are iteratively selected for expansion and moved to a closed set of states. Depending on the data structure used to represent the open set, GSEA can be instantiated as a depth-first, a breadth-first, or a directed search algorithm such as Best-First Search or A*. The proviso is characterized by reference to the open and closed set of states of the search algorithm. As a result, it can be computed in an efficient manner during the search based on local information. We implemented partial-order reduction for GSEA based on our proposed proviso in the tool HSF-SPIN, an extension of the explicit-state model checker SPIN for directed model checking. We evaluate the state space reduction achieved by partial-order reduction using the proposed proviso by comparing it on a set of benchmark problems to the use of other provisos. We also compare the use of breadth-first search (BFS) and A*, two algorithms ensuring that counterexamples of minimal length will be found, together with the proviso that we propose. -
F. Leitner and S. Leue: Simulink Design Verifier vs. SPIN - A Comparative Case Study, in: Participant's Proceedings of FMICS 2008, ERCIM Working Group on Formal Methods for Industrial Critical Systems, 2008.
Download: [PDF]Abstract: An increasing number of industrial strength software design tools come along with veri cation tools that o er some property checking capabilities. On the other hand, there is a large number of general purpose model checking tools available. The question whether users of the industrial strength design tool preferably use the built-in state space exploration tool or a general purpose model checking tool arises quite naturally. Using the case study of an AUTOSAR compliant memory management module we compare the Simulink Design Veri er and the SPIN model checking tool in terms of their suitability to verify important correctness properties of this module. The comparison is both functional in that it analyzes the suitabil- ity to verify a set of basic system properties, and quantitative in comparing the computational effciency of both tools. -
Bahareh Badhan: Prove with GDPLL-WD.
A Complete Proof Procedure for Recursive Data Structures, Technical Report soft-08-07, Chair for Software Engineering, University of Konstanz, 2008.
Download: [PDF]Abstract: In this paper we present a terminating, sound and complete algorithm for the verification of recursively defined data structures. To mention some, nat, list and tree data types and also record are commonly used examples of such structures. Recursively defined data structures are of value for use in software verification.Many programming languages support recursive data structures. The best known example on this kind is the LISP programming language, which uses list. Our algorithm, GDPLL-WD, which is an extension of the Davis, Putnam, Logemann and Loveland (DPLL) procedure solves satisfiability problem of recursive data types through providing witness assignments. -
Bahareh Badban: Culling predicates for the Verification of Real-Time Models, Technical Report soft-08-06, Chair for Software Engineering, University of Konstanz, 2008.
Download: [PDF]Abstract: We present an algorithm that generates invariants for real-time models. The algorithm, further, prunes the model by first detecting, and then removing idle discrete transitions (transitions which can never be traversed). We next demonstrate how the generated invariants can be used to create a finite-state abstraction for the original model. To this end, we enhance the idea of predicate abstraction through fully incorporating locations of the concrete timed automata model in the abstraction phase. -
Florian Leitner: Evaluation of the Matlab Simulink Design Veri er
versus the model checker SPIN, Technical Report soft-08-05, Chair for Software Engineering, University of Konstanz, 2008.
Download: [PDF]Abstract: An increasing number of industrial strength software design tools come along with verification tools that offer some property checking capabilities. On the other hand, there is a large number of general purpose model checking tools available. The question whether users of the industrial strength design tool preferably use the built-in verification tool or a general purpose model checking tool arises quite naturally. In this bachelor thesis, the Simulink Design Verifier and the SPIN model checking tool are compared. The comparison is based on the case study of an AUTOSAR compliant memory management module. The comparison is both functional in that it analyzes the suitability to verify a set of basic system properties, and quantitative in comparing the computational efficiency of both tools. In this context, it is also described how Simulink / Stateflow models can be manually translated into the input language of the model checker SPIN. -
Bahareh Badban, Wan Fokkink, Jaco van de Pol: Mechanical Verification of a Two-Way Sliding Window Protocol, Accepted for publication in the Communicating Process Architectures (CPA) conference, 2008.
Download: [PDF]Abstract: We prove the correctness of a two-way sliding window protocol with piggybacking, where the acknowledgments of the latest received data are attached to the next data transmitted back into the channel. The window size of both parties are considered to be finite, though they can be of different sizes. We show that this protocol is equivalent (branching bisimilar) to a pair of FIFO queues of finite capacities. The protocol is first modeled and manually proved for its correctness in the process algebraic language of muCRL. We use the theorem prover PVS to formalize and to mechanically prove the correctness. This implies both safety and liveness (under the assumption of fairness). -
Husain Aljazzar and Stefan Leue: Debugging of Dependability Models Using Interactive
Visualization of Counterexamples, Proceedings of 5th International Conference on the Quantitative Evaluation of SysTems (QEST), IEEE Computer Society Press, to appear, 2008.
Abstract: We present an approach to support the debugging of stochastic system models using interactive visualization. The goal of this work is to facilitate the identification of causal factors in the potentially very large sets of execution traces that form counterexamples in stochastic model checking. The visualization is interactive and allows the user to focus on the most meaningful aspects of a counterexample. We present the application of the visualization method as implemented in our prototype tool DiPro to two significant case studies. -
Husain Aljazzar and Stefan Leue: Debugging of Dependability Models Using Interactive
Visualization of Counterexamples, Technical Report soft-08-04, Chair for Software Engineering, University of Konstanz, 2008.
Download: [PDF]Abstract: We present an approach to support the debugging of stochastic system models using interactive visualization. The goal of this work is to facilitate the identification of causal factors in the potentially very large sets of execution traces that form counterexamples in stochastic model checking. The visualization is interactive and allows the user to focus on the most meaningful aspects of a counterexample. We present the application of the visualization method as implemented in our prototype tool {\sc DiPro} to two significant case studies. -
Wei Wei: Incomplete Property Checking for Asynchronous Reactive Systems, Doctoral Dissertation, University of Konstanz, 2008.
Download: [PDF]Abstract: Not available. -
Stefan Leue, Alin Stefanescu and Wei Wei: Dependency Analysis for Control Flow Cycles in Reactive Communicating Processes, Pages 176-195, Proceedings of 15th International SPIN Workshop on Model Checking of Software (SPIN '08), Lecture Notes in Computer Science, Volume 5156. Springer Verlag., 2008.
Download: [PDF]Abstract: The execution of a reactive system amounts to the repetitions of executions of control flow cycles in the component processes of the system. The way in which cycle executions are combined is not arbitrary since cycles may depend on or exclude one another. We believe that the information of such dependencies is important to the design, understanding, and verification of reactive systems. In this paper, we formally define the concept of a {\em cycle dependency}, and propose several static analysis methods to discover such dependencies. We have implemented several strategies for computing cycle dependencies and compared their performance with realistic models of considerable size. It is also shown how the detection of accurate dependencies is used to improve a livelock freedom analysis that we developed previously. -
Stefan Leue and Pedro Merino (Eds.) : Formal Methods for Industrial Critical Systems: 12th International Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised Selected Papers, LNCS 4916, Lecture Notes in Computer Science, Springer Verlag, 2008.
Abstract: Not available. -
Stefan Leue, Alin Stefanescu and Wei Wei: An AsmL Semantics for Dynamic Structures and Run Time Schedulability in UML-RT, Pages 238-257, Proceedings of 46th International Conference on Objects, Models, Components, Patterns (TOOLS '08), Lecture Notes in Business and Information Processing, Volume 11. Springer Verlag., 2008.
Download: [PDF]Abstract: Many real-time systems use runtime structural reconfiguration mechanisms based on dynamic creation and destruction of components. To support such features, UML-RT provides a set of modeling concepts including optional actor references and multiple containment. However, these concepts are not covered in any of the current formal semantics of UML-RT, thus impeding the testing and formal analysis of realistic models. We use AsmL to present an executable semantics covering dynamic structures and other important features like run time schedulability. The semantics is parametrized to capture UML-RT semantics variation points whose decision choices depend on the special implementation in a vendor CASE tool. We have built several various implementations of those variation points, including the one as implemented in the IBM Rational Rose RealTime (Rose-RT) tool. Finally, we illustrate how the proposed executable semantics can be used in the analysis of a Rose-RT model using the Spec Explorer tool. -
Husain Aljazzar and Stefan Leue: K*: A Directed On-The-Fly Algorithm for Finding the k Shortest Paths, Technical Report soft-08-03, Chair for Software Engineering, University of Konstanz, 2008.
Download: [PDF]Abstract: We present a new algorithm, called K$^*$, for finding the $k$ shortest paths between a designated pair of vertices in a given directed weighted graph. Compared to Eppstein's algorithm, which is the most prominent algorithm for solving this problem, K$^*$ has two advantages. First, K$^*$ performs on-the-fly, which means that it does not require the graph to be explicitly available and stored in main memory. Portions of the graph will be generated as needed. Second, K$^*$ is a directed algorithm which enables the use of heuristic functions to guide the search. This leads to significant improvements in the memory and runtime demands for many practical problem instances. We prove the correctness of K$^*$ and show that it maintains a worst-case runtime complexity of $\mathcal{O}(m + k\,n\,log(k\,n))$ and a space complexity of $\mathcal{O}(k\,n + m)$, where $n$ is the number of vertices and $m$ is the number of edges of the graph. We provide experimental results which illustrate the scalability of the algorithm. -
Stefan Leue, Alin Stefanescu and Wei Wei: An AsmL Semantics for Dynamic Structures and Run Time Schedulability in UML-RT (Long Version), Technical Report soft-08-02, Chair for Software Engineering, University of Konstanz, 2008.
Download: [PDF]Abstract: Many real-time systems use runtime structural reconfiguration mechanisms based on dynamic creation and destruction of components. To support such features, UML-RT provides a set of modeling concepts including optional actor references and multiple containment. However, these concepts are not covered in any of the current formal semantics of UML-RT, thus impeding the testing and formal analysis of realistic models. We use AsmL to present an executable semantics covering dynamic structures and other important features like run time schedulability. The semantics is parametrized to capture UML-RT semantics variation points whose decision choices depend on the special implementation in a vendor CASE tool. We have built several various implementations of those variation points, including the one as implemented in the IBM Rational Rose RealTime (Rose-RT) tool. Finally, we illustrate how the proposed executable semantics can be used in the analysis of a Rose-RT model using the Spec Explorer tool. -
Husain Aljazzar and Stefan Leue: Counterexamples for Model Checking of Markov Decision Processes, Technical Report soft-08-01, Chair for Software Engineering, University of Konstanz, 2007.
Download: [PDF]Abstract: The debugging of stochastic system models relies on the availability of diagnostic information. Classic probabilistic model checkers, which are based on iterated numerical probability matrix operations, do not provide such diag- nostic information. In precursory work, we have devised counterexample genera- tion methods for continuous- and discrete-time Markov Chains based on heuris- tics guided explicit state space search. In this paper we address the problem of generating diagnostic information, or counterexamples, for Markov Decision Processes (MDPs), which are a convenient formalism for modelling concurrent stochastic systems. We define the notion of counterexamples for MDPs in re- lation to an upwards-bounded PCTL formula. Next we present our approach to counterexample generation. We first use an adoption of Eppstein’s algorithm for k-shortest paths in order to collect the most probable MDP execution traces contributing to a violation of the PCTL formula.We then use the data structure of AND/OR trees in order to adequately extract from the collected execution sequences the most informative counterexample and to compute its probability. In our experimental evaluation we show that our approach scales to models of realistic size, and that the collected diagnostic information is helpful in system debugging. -
Dragan Bosnacki, Stefan Leue, and Alberto Lluch Lafuente: Partial-Order Reduction for General State Exploring Algorithms, To appear in: International Journal on Software Tools for Technology Transfer, 2007.
Download: [PDF]Abstract: Partial-Order Reduction is one of the main techniques used to tackle the combinatorial state explosion problem occurring in explicit-state model checking of concurrent systems. The reduction is performed by exploiting the independence of concurrently executed events which allows portions of the state space to be pruned. An important condition for the soundness of partial-order based reduction algorithms is a condition that prevents indefinite ignoring of actions when pruning the state space. This condition is commonly known as the cycle proviso. In this paper we present a new version of this proviso which is applicable to a general search algorithm skeleton that we refer to as the General State Expanding Algorithm (GSEA). GSEA maintains a set of open states from which states are iteratively selected for expansion and moved to a closed set of states. Depending on the data structure used to represent the open set, GSEA can be instantiated as a depth-first, a breadthfirst, or a directed search algorithm such as Best-First Search or A*. The proviso is characterized by reference to the open and closed set of states of the search algorithm. As a result it can be computed in an efficient manner during the search based on local information.We implemented partial-order reduction for GSEA based on our proposed proviso in the tool HSF-SPIN, an extension of the explicit-state model checker SPIN for directed model checking. We evaluate the state space reduction achieved by partial-order reduction using the proposed proviso by comparing it on a set of benchmark problems to the use of other provisos. We also compare the use of breadth-first search (BFS) and A*, two algorithms ensuring that counterexamples of minimal length will be found, together with the proviso that we propose. -
Giuseppe di Fatta, Stefan Leue and Evghenia Stegantova: Discriminative Pattern Mining in Software Fault Detection, Proceedings of the Third International Workshop on Software Quality Assurance SOQUA'06, ACM Digital Library, 2006.
Download: [PDF]Abstract: We present a method to enhance fault localization for software systems based on a frequent pattern mining algorithm. Our method is based on a large set of test cases for a given set of programs in which faults can be detected. The test executions are recorded as function call trees. Based on test oracles the tests can be classi ed into successful and failing tests. A frequent pattern mining algorithm is used to identify frequent subtrees in successful and failing test executions. This information is used to rank functions according to their likelihood of containing a fault. The ranking suggests an order in which to examine the functions during fault analysis. We validate our approach experimentally using a subset of Siemens benchmark programs. -
Husain Aljazzar and Stefan Leue: Extended Directed Search for Probabilistic Timed Reachability, Pages 33-51, Proceedings of 4th International Conference on Formal Modelling and Analysis of Timed Systems FORMATS '06, Lecture Notes in Computer Science, Springer Verlag, 2006.
Download: [PDF]Abstract: Current numerical model checkers for stochastic systems can efficiently analyse stochastic models. However, the fact that they are unable to provide debugging information constrains their practical use. In precursory work we proposed a method to select diagnostic traces, in the parlance of functional model checking commonly referred to as failure traces or counterexamples, for probabilistic timed reachability properties on discrete-time and continuous-time Markov chains. We applied directed explicit-state search algorithms, like Z∗, to determine a diagnostic trace which carries large amount of probability. In this paper we extend this approach to determining sets of traces that carry large probability mass, since properties of stochastic systems are typically not violated by single traces, but by collections of those. To this end we extend existing heuristics guided search algorithms so that they select sets of traces. The result is provided in the form of a Markov chain. Such diagnostic Markov chains are not just essential tools for diagnostics and debugging but, they also allow the solution of timed reachability probability to be approximated from below. In particular cases, they also provide real counterexamples which can be used to show the violation of the given property. Our algorithms have been implemented in the stochastic model checker PRISM. We illustrate the applicability of our approach using a number of case studies. -
Stefan Leue, Alin Stefanescu, and Wei Wei: A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems, Pages 79-94, Proceedings of 17th International Conference on Concurrency Theory CONCUR '06, LNCS 4137, Lecture Notes in Computer Science, Springer Verlag., 2006.
Download: [PDF]Abstract: We describe an incomplete but sound and efficient livelock freedom test for infinite state asynchronous reactive systems. The method abstracts a system into a set of simple control flow cycles labeled with their message passing effects. From these cycles, it constructs a homogeneous integer programming problem (IP) encoding a necessary condition for the existence of livelock runs. Livelock freedom is assured by the infeasibility of the generated homogeneous IP, which can be checked in polynomial time. In the case that livelock freedom cannot be proved, the method proposes a counterexample given as a set of cycles. We apply an automated cycle dependency analysis to counterexamples to check their spuriousness and to refine the abstraction. We illustrate the application of the method to Promela models using our prototype implementation named aLive. -
Husain Aljazzar and Stefan Leue: Extended Directed Search for Probabilistic Timed Reachability, Technical Report soft-06-03, Chair for Software Engineering, University of Konstanz, 2006.
Download: [PDF]Abstract: Currently, stochastic model checkers can efficiently analyse stochastic models. However, they are unable to provide debugging information in the form of offending system traces, in model checking parlance commonly referred to as counterexamples. This constrains the practical use of stochastic model checking. We propose a method to select counterexamples for probabilistic timed reachability properties on discrete-time and continuous-time Markov chains. We employ directed explicit-state search algorithms, e.g. BF and Z∗, to determine failure traces which carry large amounts of probability mass. For this purpose we introduce a probabilistic evaluation function to measure the quality of failure traces. For the debugging of probabilistic reachability it is usually inevitable to consider sets of failure traces. Thus, we extend the standard algorithms in order to select failure subgraphs. Such failure subgraphs are not just essential tools for debugging but, in particular cases, they also provide real counterexamples which can be used to show the violation of the given property. They also allow the solution of timed probabilistic reachability properties to be approximated from below. To illustrate our approach we apply it to probabilistic models of some case studies. -
Stefan Leue, Alin Stefanescu, and Wei Wei: A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems, Technical Report soft-06-02, Chair for Software Engineering, University of Konstanz, 2006.
Download: [PDF]Abstract: We describe an incomplete but sound and efficient livelock freedom test for infinite state asynchronous reactive systems. The method abstracts a system into a set of simple control flow cycles labeled with their message passing effects. From these cycles, it constructs a homogeneous integer programming problem (IP) encoding a necessary condition for the existence of livelock runs. Livelock freedom is assured by the infeasibility of the generated homogeneous IP, which can be checked in polynomial time. In the case that livelock freedom cannot be proved, the method proposes a counterexample given as a set of cycles. We apply an automated cycle dependency analysis to counterexamples to check their spuriousness and to refine the abstraction. We illustrate the application of the method to Promela models using our prototype implementation named aLive. -
Dragan Bosnacki, Stefan Leue, and Alberto Lluch Lafuente: Partial-Order Reduction for General State Exploring Algorithms, Pages 271-287, Proceedings of the 13th International SPIN Workshop on Model Checking of Software, LNCS 3925, Lecture Notes in Computer Science, Springer Verlag, 2006.
Download: [PDF]Abstract: An important component of partial-order based reduction algorithms is the condition that prevents action ignoring, commonly known as the cycle proviso. In this paper we give a new version of this proviso that is applicable to a general search algorithm skeleton also known as the General State Expanding Algorithm (GSEA). GSEA maintains a set of open (visited but not expanded) states from which states are iteratively selected for exploration and moved to a closed set of states (visited and expanded). Depending on the open set data structure used, GSEA can be instantiated as depth-first, breadth-first, or a directed search algorithm. The proviso is characterized by reference to the open and closed set of states in GSEA. As a result the proviso can be computed in an efficient manner during the search based on local information. We implemented partial-order reduction for GSEA based on our proposed proviso in the tool HSF-SPIN, which is an extension of the model checker SPIN for directed model checking. We evaluate the state space reduction achieved by partial-order reduction according to the proviso that we propose by comparing it on a set of benchmark problems to other reduction approaches. -
Stefan Leue and Wei Wei: A Region Graph Based Approach to Termination Proofs, Technical Report soft-06-01, Chair for Software Engineering, University of Konstanz, 2006.
Download: [PDF]Abstract: Automated termination proofs are indispensable in the mechanic verification of many program properties. While most of the recent work on automated termination proofs focuses on the construction of linear ranking functions, we develop an approach based on region graphs in which regions define subsets of variable values that have different effects on loop termination. In order to establish termination, we check whether (1) any region will be exited once it is entered, and (2) no region is entered an infinite number of times.We show the effectiveness of our proof method by experiments with Java code using a prototype implementation of our approach. -
Stefan Leue and Wei Wei: A Region Graph Based Approach to Termination Proofs, Pages 318-333, Proceedings of 12th. International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS '06, LNCS 3920, Lecture Notes in Computer Science, Springer Verlag, 2006.
Download: [PDF]Abstract: Automated termination proofs are indispensable in the mechanic verification of many program properties. While most of the recent work on automated termination proofs focuses on the construction of linear ranking functions, we develop an approach based on region graphs in which regions define subsets of variable values that have different effects on loop termination. In order to establish termination, we check whether (1) any region will be exited once it is entered, and (2) no region is entered an infinite number of times.We show the effectiveness of our proof method by experiments with Java code using a prototype implementation of our approach. -
Dragan Bosnacki, Stefan Leue, and Alberto Lluch Lafuente: Partial-Order Reduction for General State Exploring Algorithms, Technical Report soft-05-02, Chair for Software Engineering, University of Konstanz, 2005.
Download: [PDF]Abstract: An important component of partial-order based reduction algorithms is the condition that prevents action ignoring, commonly known as the cycle proviso. In this paper we give a new version of this proviso that is applicable to a general search algorithm skeleton also known as the General State Expanding Algorithm (GSEA). GSEA maintains a set of open (visited but not expanded) states from which states are iteratively selected for exploration and moved to a closed set of states (visited and expanded). Depending on the open set data structure used, GSEA can be instantiated as depth-first, breadth-first, or a directed search algorithm. The proviso is characterized by reference to the open and closed set of states in GSEA. As a result the proviso can be computed in an efficient manner during the search based on local information. We implemented partial-order reduction for GSEA based on our proposed proviso in the tool HSF-SPIN, which is an extension of the model checker SPIN for directed model checking. We evaluate the state space reduction achieved by partial-order reduction according to the proviso that we propose by comparing it on a set of benchmark problems to other reduction approaches. -
Husain Aljazzar, Holger Hermanns, and Stefan Leue: Counterexamples for Timed Probabilistic Reachability, Pages 177-195, Proceedings of the 3rd International Conference on Formal Modelling and Analysis of Timed Systems FORMATS'05, LNCS 3829, Lecture Notes in Computer Science, Springer Verlag, 2005.
Download: [PDF]Abstract: The inability to provide counterexamples for the violation of timed probabilistic reachability properties constrains the practical use of CSL model checking for continuous time Markov chains (CTMCs). Counterexamples are essential tools in determining the causes of property violations and are required during debugging. We propose the use of explicit state model checking to determine runs leading into property offending states. Since we are interested in finding paths that carry large amounts of probability mass we employ directed explicit state model checking technology to find such runs using a variety of heuristics guided search algorithms, such as Best First search and Z*. The estimates used in computing the heuristics rely on a uniformisation of the CTMC. We apply our approach to a probabilistic model of the SCSI-2 protocol. -
Stefan Leue and Tarja Johanna Systä (Eds.): Scenarios: Models, Transformations and Tools: Proceedings of International Workshop Dagstuhl Castle, Germany, September 2003, LNCS 3466, Lecture Notes in Computer Science, Springer Verlag, 2005.
Abstract: Not available. -
Stefan Leue and Wei Wei: Counterexample-based Refinement for a Boundedness
Test for CFSM Languages, Pages 58-74, Proceedings of 12th International SPIN Workshop on Model Checking of Software SPIN2005, LNCS 3639, Lecture Notes in Computer Science, Springer Verlag, 2005.
Download: [PDF]Abstract: In precursory work we suggested an abstraction-based highly scalable semi-test for the boundedness of Communicating Finite State Machine (CFSM) based modelling and programming languages. We illustrated its application to Promela and UML-RT models. The test is sound with respect to determining boundedness, but may return inconclusive counterexamples when boundedness cannot be established. In this paper we turn to the question how to effectively determine the spuriousness of these counterexamples, and how to refine the abstraction based on the analysis. We employ methods from program analysis and illustrate the application of our refinement method to a number of Promela examples. -
Stefan Leue and Wei Wei: Counterexample Refinement for a Boundedness Test for CFSM Languages, Technical Report soft-05-01, Chair for Software Engineering, University of Konstanz, 2005.
Download: [PDF]Abstract: In precursory work we suggested an abstraction-based highly scalable semi-test for the boundedness of Communicating Finite State Machine (CFSM) based modelling and programming languages. We illustrated its application to Promela and UML-RT models. The test is sound with respect to determining boundedness, but may return inconclusive counterexamples when boundedness cannot be established. In this paper we turn to the question how to effectively determine the spuriousness of these counterexamples, and how to refine the abstraction based on the analysis. We employ methods from program analysis and illustrate the application of our refinement method to a number of Promela examples. -
Matthew Dwyer and Stefan Leue: The Algorithmics of Software Model Checking (Introductory Paper), Pages 257-259, International Journal on Software Tools for Technology Transfer 6 (4), Springer Verlag, 2004.
Download: [PDF]Abstract: Not available. -
Jianbin Tan, George S. Avrunin, Lori A. Clarke, Shlomo Zilberstein, and Stefan Leue: Heuristic-Guided Counterexample Search in FLAVERS, Pages 201-210, Proceedings of the 12th ACM Symposium on the Foundations of Software Engineering, ACM Press, 2004.
Download: [PDF]Abstract: One of the benefits of finite-state verification (FSV) tools, such as model checkers, is that a counterexample is provided when the property cannot be verified. Not all counterexamples, however, are equally useful to the analysts trying to understand and localize the fault. Often counterexamples are so long that they are hard to understand. Thus, it is important for FSV tools to find short counterexamples and to do so quickly. Commonly used search strategies, such as breadth-first and depth-first search, do not usually perform well in both of these dimensions. In this paper, we investigate heuristic-guided search strategies for the FSV tool FLAVERS and propose a novel two-stage counterexample search strategy. We describe an experiment showing that this two-stage strategy, when combined with appropriate heuristics, is extremely effective at quickly finding short counterexamples for a large set of verification problems. -
Stefan Edelkamp, Stefan Leue, and Alberto Lluch-Lafuente: Partial-Order Reduction and Trail Improvement in Directed Model Checking, Pages 277-301, International Journal on Software Tools for Technology Transfer 6 (4), Springer Verlag, 2004.
Download: [PDF]Abstract: In this paper we present work on trail improvement and partial-order reduction in the context of directed explicit-state model checking. Directed explicitstate model checking employs directed heuristic search algorithms such as A* or best-first search to improve the error-detection capabilities of explicit-state model checking. We first present the use of directed explicit-state model checking to improve the length of already established error trails. Second, we show that partial-order reduction, which aims at reducing the size of the state space by exploiting the commutativity of concurrent transitions in asynchronous systems, can coexist well with directed explicit-state model checking. Finally, we illustrate how to mitigate the excessive length of error trails produced by partial-order reduction in explicit-state model checking. In this context we also propose a combination of heuristic search and partial-order reduction to improve the length to already provided counterexamples. -
Stefan Leue, Richard Mayr, and Wei Wei: A Scalable Incomplete Test for Message Buffer Overflow in Promela Models, Pages 216-233, Proceedings of the 11th International SPIN Workshop on Model Checking Software SPIN 2004, LNCS 2989, Lecture Notes in Computer Science, Springer Verlag, 2004.
Download: [PDF]Abstract: In Promela, communication buffers are defined with a fixed length, and buffer overflows can be handled in two different ways: block the send statement or lose the message. Both solutions change the semantics of the system, compared to one with unbounded channels. The question arises, if such buffer overflows can ever occur in a given system and what buffer lengths are sufficient to avoid them. We describe a scalable incomplete boundedness test for the communication buffers in Promela models, which is based on overapproximation and static analysis.We first reduce Promela models to systems of communicating finite state machines (CFSMs) and then apply further abstractions that leave us with a system of linear inequalities. Those represent the message sending and receiving effect that the control flow cycles of every process have on any message buffer. The test tries to establish the existence of a linear combination of the effect vectors so that at least one message can occur an unbounded number of times. If no such linear combination exists then the system is bounded. We discuss the complexity of this test and present experimental results using our implementation in the IBOC system. Scalability of the test is in part due to the fact that it is polynomial for the type of sparse control flowgraphs derived from Promela models. Also, the analysis is local, i.e., it avoids the combinatorial state space explosion due to concurrency of the models. We also present a method to derive upper bound estimates for the maximal occupancy of each individual message buffer. Previously, we have applied this approach to UML RT models, while in this paper we focus on the additional problems specific to Promela code: determining the potential message types of any channel, tracking potential contents of variables, channels passed as arguments to processes, channel assignments, channel arrays and parallel process creation. -
Stefan Leue, Richard Mayr, and Wei Wei: A Scalable Incomplete Test for the Boundedness of UML RT Models, Pages 327-341, Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2004, LNCS 2988, Lecture Notes in Computer Science, Springer Verlag, 2004.
Download: [PDF]Abstract: We describe a scalable incomplete boundedness test for the communication buffers in UML RT models. UML RT is a variant of the UML modeling language, tailored to describing asynchronous concurrent embedded systems. We reduce UML RT models to systems of communicating finite state machines (CFSMs). We propose a series of further abstractions that leaves us with a system of linear inequalities. Those represent the message sending and receiving effect that the control flow cycles of every process have on the overall message buffer. The test tries to establish the existence of a linear combination of the effect vectors so that at least one message can occur an unbounded number of times. We discuss the complexity of this test and present experimental results using the IBOC system that we are implementing. Scalability of the test is in part due to the fact that it is polynomial for the type of sparse control flow graphs that are derived from UML RT models. Also, the analysis is local, i.e., it avoids the combinatorial state space explosion due to concurrency of the models.We also present a method to derive upper bound estimates for the maximal occupancy of each individual message buffer. While we focus on the analysis of UML RT models, the analysis can directly be applied to any type of CFSM models. -
Stefan Edelkamp, Stefan Leue, and Alberto Lluch-Lafuente: Directed Explicit-State Model Checking in the Validation of Communication Protocols, Pages 247-267, International Journal on Software Tools for Technology Transfer 5 (2-3), Springer Verlag, 2004.
Download: [PDF]Abstract: The success of model checking is largely based on its ability to efficiently locate errors in software designs. If an error is found, a model checker produces a trail that shows how the error state can be reached, which greatly facilitates debugging. However, while current model checkers find error states efficiently, the counterexamples are often unnecessarily lengthy, which hampers error explanation. This is due to the use of “naive” search algorithms in the state space exploration. In this paper we present approaches to the use of heuristic search algorithms in explicit-state model checking. We present the class of A* directed search algorithms and propose heuristics together with bitstate compression techniques for the search of safety property violations. We achieve great reductions in the length of the error trails, and in some instances render problems analyzable by exploring a much smaller number of states than standard depth-first search. We then suggest an improvement of the nested depth-first search algorithm and show how it can be used together with A* to improve the search for liveness property violations. Our approach to directed explicit-state model checking has been implemented in a tool set called HSF-SPIN. We provide experimental results from the protocol validation domain using HSF-SPIN. -
Peter Biechele and Stefan Leue: Explicit State Model Checking in the Development Process for Inter-locking Software Systems (Extended Abstract), Proceedings of the Workshop on Model-Checking for Dependable Software-Intensive Systems to be held at the IEEE/IFIP International Conference on Dependable Systems and Networks, San Francisco, USA, 2003.
Download: [PDF]Abstract: We report on an ongoing project that addresses the use of explicit state model checking technology in the design of railroad interlocking systems. We discuss our modeling approach, the requirements on the use of formal methods as specified in the pertinent CENELEC standards, and the use of explicit state model checking in requirements verification and test case generation. In the context of test case generation we also illustrate the use of heuristic search strategies in model checking. -
Dragan Bosnacki and Stefan Leue (Eds.): Proceedings of the 9th International SPIN Workshop on Model Checking of Software, Volume 2318, Lecture Notes in Computer Science, Springer Verlag, 2002.
Abstract: Not available. -
Alberto Lluch-Lafuente, Stefan Edelkamp, Stefan Leue: Partial Order Reduction in Directed Model Checking, Volume 2318, Pages 112-127, Proceedings of the 9th International SPIN Workshop on Software Model Checking, Lecture Notes in Computer Science, Springer Verlag, 2002.
Download: [PDF] [PS]Abstract: Partial order reduction is a very succesful technique for avoiding the state explosion problem that is inherent to explicit state model checking of asynchronous concurrent systems. It exploits the commutativity of concurrently executed transitions in interleaved system runs in order to reduce the size of the explored state space. Directed model checking on the other hand addresses the state explosion problem by using guided search techniques during state space exploration. As a consequence, shorter errors trails are found and less search effort is required than when using standard depth-first or breadth-first search. We analyze how to combine directed modelchecking with partial order reduction methods and give experimental results on how the combination of both techniques performs. -
Stefan Edelkamp, Alberto Lluch Lafuente and Stefan Leue: Protocol Verification with Heuristic Search, Pages 75-83, Proceedings of the AAAI-Spring Symposium on Model-based Validation of Intelligence, Stanford University, 2001.
Download: [PDF] [PS]Abstract: We present an approach to reconcile explicit state model checking and heuristic directed search. We provide experimental evidence that the model checking problem for concurrent systems, such as communications protocols, can be solved more efficiently, since finding a state violating a property can be understood as a directed search problem. In our work we combine the expressive power and implementation efficiency of the SPIN model checker with the HSF heuristic search workbench, yielding the HSF-SPIN tool that we have implemented. We start off from the A* algorithm and some of its derivatives and define heuristics for various system properties that guide the search so that it finds error states faster. In this paper we focus on safety properties and provide heuristics for invariant and assertion violation and deadlock detection. We provide experimental results for applying HSF-SPIN to two toy protocols and one real world protocol, the CORBA GIOP protocol. -
Stefan Edelkamp, Alberto Lluch Lafuente, Stefan Leue: Directed Explicit Model Checking with HSF-SPIN, Pages 57-79, Proceedings of 8th International SPIN Workshop on Model Checking Software, LNCS 2057, Lecture Notes in Computer Science, Springer Verlag, 2001.
Download: [PDF] [PS]Abstract: We present the explicit state model checker HSF-SPIN which is based on the model checker SPIN and its Promela modeling language. HSF-SPIN incorporates directed search algorithms for checking safety and a large class of LTL-specified liveness properties. We start off from the A* algorithm and define heuristics to accelerate the search into the direction of a specified failure situation. Next we propose an improved depth-first search algorithm that exploits the structure of Promela Never-Claims. As a result of both improvements, counterexamples will be shorter and the explored part of the state space will be smaller than with classical approaches, allowing to analyze larger state spaces. We evaluate the impact of the new heuristics and algorithms on a set of protocol models, some of which are real-world industrial protocols. -
Stefan Edelkamp, Alberto Luch Lafuente and Stefan Leue: Trail-Directed Model Checking, Pages 343-356, Proceedings of the Workshop on Software Model Checking, Electrical Notes in Theoretical Computer Science 55 (3), Elsevier, 2001.
Download: [PDF]Abstract: HSF-SPIN is a Promela model checker based on heuristic search strategies. It utilizes heuristic estimates in order to direct the search for finding software bugs in concurrent systems. As a consequence, HSF-SPIN is able to find shorter trails than blind depth-first search. This paper contributes an extension to the paradigm of directed model checking to shorten already established unacceptable long error trails. This approach has been implemented in HSF-SPIN. For selected benchmark and industrial communication protocols experimental evidence is given that trail-directed model-checking effectively shortcuts existing witness paths. -
Stefan Edelkamp, Stefan Leue, Alberto Lluch-Lafuente: Partial Order Reduction in Directed Model Checking, Technical Report No. 162, Institute for Computer Science, Albert-Ludwigs-University Freiburg, 2001.
Download: [PDF] [PS]Abstract: Partial order reduction is one of the most effective techniques for avoiding the state explosion problem that is inherent to explicit state model checking of asynchronous concurrent systems. It exploits the commutativity of concurrently executed transitions in interleaved system runs in order to reduce the size of the explored state space. Directed model checking on the other hand addresses the state explosion problem by using guided search techniques during state space exploration. As a consequence shorter errors trails are found and less search effort is required than when using standard depth-first or breadth-first search. We analyze how to combine directed model checking with partial order reduction methods and give experimental results on how the combination of both techniques perform. -
Stefan Edelkamp, Stefan Leue, Alberto Lluch-Lafuente: Directed Explicit-State Model Checking in the Validation of Communication Protocols, Technical Report No. 161, Institute for Computer Science, Albert-Ludwigs-University Freiburg, 2001.
Download: [PDF] [PS]Abstract: The success of model checking is largely based on its ability to efficiently locate errors in software designs. If an error is found, a model checker produces a trail that shows how the error state can be reached, which greatly facilitates debugging. However, while current model checkers find error states efficiently, the counterexamples are often unnecessarily lengthy, which hampers error explanation. This is due to the use of "naive" search algorithms in the state space exploration. In this paper we present approaches to the use of heuristic search algorithms in explicit-state model checking. We present the class of A* directed search algorithms and propose heuristics together with bitstate compression techniques for the search of safety property violations. We achieve great reductions in the length of the error trails, and in some instances render problems analyzable by exploring a much smaller number of states than standard depth-first search. We then suggest an improvement of the nested depth-first search algorithm and show how it can be used together with A* to improve the search for liveness property violations. Our approach to directed explicit-state model checking has been implemented in a tool set called HSF-SPIN. We provide experimental results from the protocol validation domain using HSF-SPIN. -
Moataz Kamel and Stefan Leue: Formalization and Validation of the General Inter-ORB Protocol (GIOP) using Promela and Spin, Pages 394-409, International Journal on Software Tools for Technology Transfer 2 (4), Springer Verlag, 2000.
Download: [PDF]Abstract: The General Inter-Orb Protocol (GIOP) is a key component of the Common Object Request Broker Architecture (CORBA) specification. We present the formal modeling and validation of the GIOP protocol using the Promela language, Linear Time Temporal Logic (LTL) and the Spin model checker. We validate the Promela model using ten high-level requirements which we elicit from the informal CORBA specification. These requirements are then formalized in LTL and the Spin model checker is used to determine their validity. During the validation process we discovered a few problems in GIOP: a potential transport-layer interface deadlock and problems with the server migration protocol. We also describe how property specification patterns helped us in formalizing the high-level requirements that we have elicited. -
Moataz Kamel and Stefan Leue: VIP: A Visual Editor and Compiler for v-Promela, Pages 471-486, Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2000, LNCS 1785, Lecture Notes in Computer Science, Springer Verlag, 2000.
Download: [PDF] [PS]Abstract: We describe the Visual Interface to Promela (VIP) tool that we have recently implemented. VIP supports the visual editing and maintenance of v-Promela models. v-Promela is a visual, object-oriented extension to Promela, the input language to the Spin~model checker. We introduce the v-Promela notation as supported by the VIP editor, discuss Promela code generation, and describe the process of property validation for the resulting models. Our discussion centers around two case studies, a call processing system and the CORBA GIOP protocol. -
P. Tysowski, Mohammad Zulkernine and Stefan Leue: JaCal: An Implementation of Linda in Java, Pages 683-692, Proceedings of the IASTED Conference on Parallel and Distributed Computing and Systems PDCS '99, Cambridge, 1999.
Abstract: Not available. -
Dennis Dams, Rob Gerth, Stefan Leue, and Mieke Massink (Eds.): Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, LNCS 1680, Lecture Notes in Computer Science, Springer Verlag, 1999.
Abstract: Not available. -
Stefan Leue and Gerard Holzmann: v-Promela: A Visual, Object-Oriented Language for Spin, Pages 14-23, Proceedings of the Second IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, Saint Malo, France, IEEE Computer Society Press, 1999.
Download: [PDF] [PS]Abstract: We describe the design of VIP, a graphical front-end to the model checker Spin. VIP supports a visual formalism, called v-Promela that connects the model checker to modern hierarchical notations for the specification of object-oriented, reactive systems. The formalism is comparable to formalisms such as UML-RT, ROOM, and Statecharts, but is presented here in a framework that allows us to combine the benefits of a visual, hierarchical specification method with the power of LTL model checking provided by Spin. Like comparable formalisms, VIP can describe hierarchies of behaviour and of system structure. The formalism is designed to be transparent to the Spin model checker itself, by allowing all central constructs to be translated mechanically into basic Promela, as already supported by the existing model checker. -
Moataz Kamel and Stefan Leue: Validation of Remote Object Invocation and Object Migration in CORBA GIOP using Promela/Spin, Actes/Proceedings Spin\'98, Ecole Nationale Superieure des Telecommunications, Paris, France, 1998.
Abstract: Not available. -
Hanêne Ben-Abdallah and Stefan Leue: MESA: Support for Scenario-Based Design of Concurrent Systems
, Volume 1384, Pages 118 - 135, Lecture Notes in Computer Science, Springer Verlag, 1998.
Download: [PDF] [PS]Abstract: The latest ITU-T standard syntax of Message Sequence Charts (MSCs) offers several operators to compose MSCs in a hierarchical, iterating, and nondeterministic way. However, current tools operate on MSCs that describe finite, deterministic behavior. In this paper, we describe the architecture and the partial implementation of Mesa, an MSC-based tool that supports early phases of the software development cycle. The main functionalities of MESA are: an environment for the composition of system models through MSCs, syntactic and model-based analysis of an MSC model, and resolution of resource related underspecifications in an MSC model. -
Hanêne Ben-Abdallah and Stefan Leue: MESA: Support for Scenario-Based Design of Concurrent Systems
, Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'98, 1998.
Download: [PDF] [PS]Abstract: The latest ITU-T standard syntax of Message Sequence Charts (MSCs) offers several operators to compose MSCs in a hierarchical, iterating, and nondeterministic way. However, current tools operate on MSCs that describe finite, deterministic behavior. In this paper, we describe the architecture and the partial implementation of Mesa, an MSC-based tool that supports early phases of the software development cycle. The main functionalities of MESA are: an environment for the composition of system models through MSCs, syntactic and model-based analysis of an MSC model, and resolution of resource related underspecifications in an MSC model. -
Stefan Leue, Lars Mehrmann and Mohammad Rezai: Synthesizing ROOM Models from Message Sequence Chart Specifications
, 13th IEEE Conference on Automated Software Engineering, Honolulu, Hawaii, 1998.
Download: [PDF] [PS]Abstract: Message Sequence Chart (MSC) specifications have found their way into many software engineering methodologies and CASE tools, in particular in the area of telecommunications and concurrent real-time systems. MSC Specifications often represent early life-cycle requirements and high-level design specifications. We are considering iterating and branching MSC specifications according to ITU-T Recommendation Z.120. We show how these specifications can be analyzed with respect to their software architectural content, including structure and behaviour. We present algorithms for the automated synthesis of Real-Time Object-Oriented Modeling (ROOM) models from MSC specifications and discuss their implementation in the Mesa toolset. The automation of the synthesis contributes to making the transition from high-level, message exchange-oriented views to the level of a full life-cycle architecture description more efficient and reliable. This means that we are contributing to making Z.120 MSC specifications more useful in the software engineering process. -
Stefan Leue, Lars Mehrmann and Mohammad Rezai: Synthesizing ROOM Models from Message Sequence Chart Specifications
, Technical Report 98-06, Dept. of Electrical and Computer Engineering, University of Waterloo, 1998.
Download: [PDF] [PS]Abstract: Message Sequence Chart (MSC) specifications have found their way into many software engineering methodologies and CASE tools, in particular in the area of telecommunications and concurrent real-time systems. MSC Specifications often represent early life-cycle requirements and high-level design specifications. We are considering iterating and branching MSC specifications according to ITU-T Recommendation Z.120. We show how these specifications can be analyzed with respect to their software architectural content, including structure and behaviour. We present algorithms for the automated synthesis of Real-Time Object-Oriented Modeling (ROOM) models from MSC specifications and discuss their implementation in the Mesa toolset. The automation of the synthesis contributes to making the transition from high-level, message exchange-oriented views to the level of a full life-cycle architecture description more efficient and reliable. This means that we are contributing to making Z.120 MSC specifications more useful in the software engineering process. -
Stefan Fischer and Stefan Leue: Formal Methods for Broadband and Multimedia Systems
, Technical Report 97-08, Department of Electrical and Computer Engineering, University of Waterloo., 1997.
Download: [PDF] [PS]Abstract: The proper capture of desired system properties is a pivotal step in providing high quality systems. The formal specification of these properties is necessary to provide unambiguous documentation as well as automated transformation of system requirements during all stages of the life cycle. The standardized Formal Description Techniques (FDTs) Estelle and SDL have proved useful for the specification of traditional protocols and distributed systems. With the availability of high-speed networks new applications with additional requirements and characteristics are becoming reality. These requirements are often referred to as {\em Quality of Service} (QoS) requirements. We show that the above mentioned FDTs do not possess the expressiveness to capture important classes of QoS requirements, namely quantitative deterministic real-time-related properties. It is the purpose of this paper to exemplify steps that need to be taken in order to overcome this deficit. We first discuss choices that need to be made when designing a suitable real-time execution model for SDL and Estelle and proceed to present two remedies to the inexpressiveness problem: First, we introduce the concept of complementary real-time specification by reconciling the semantic models of Metric Temporal Logic and SDL and showing how both languages can be used in a complementary fashion. Second, we suggest a language extension and the corresponding semantic interpretation for Estelle. While we present examples from the domain of multimedia and broadband systems, the applicability of our specification methods extends to hard real-time systems. Finally, we discuss extensions of our techniques to capture QoS stochastic properties, and we allude to formal requirements verification and automatic implementation based on our techniques. -
Stefan Fischer and Stefan Leue: Formal Methods for Broadband and Multimedia Systems
, Computer Networks and ISDN Systems, 1997.
Download: [PDF] [PS]Abstract: The proper capture of desired system properties is a pivotal step in providing high quality systems. The formal specification of these properties is necessary to provide unambiguous documentation as well as automated transformation of system requirements during all stages of the life cycle. The standardized Formal Description Techniques (FDTs) Estelle and SDL have proved useful for the specification of traditional protocols and distributed systems. With the availability of high-speed networks new applications with additional requirements and characteristics are becoming reality. These requirements are often referred to as {\em Quality of Service} (QoS) requirements. We show that the above mentioned FDTs do not possess the expressiveness to capture important classes of QoS requirements, namely quantitative deterministic real-time-related properties. It is the purpose of this paper to exemplify steps that need to be taken in order to overcome this deficit. We first discuss choices that need to be made when designing a suitable real-time execution model for SDL and Estelle and proceed to present two remedies to the inexpressiveness problem: First, we introduce the concept of complementary real-time specification by reconciling the semantic models of Metric Temporal Logic and SDL and showing how both languages can be used in a complementary fashion. Second, we suggest a language extension and the corresponding semantic interpretation for Estelle. While we present examples from the domain of multimedia and broadband systems, the applicability of our specification methods extends to hard real-time systems. Finally, we discuss extensions of our techniques to capture QoS stochastic properties, and we allude to formal requirements verification and automatic implementation based on our techniques. -
Peter B. Ladkin and Stefan Leue: Implementing and Verifying MSC Specifications Using Promela/XSpin
, Volume 32, Proceedings of the DIMACS Workshop SPIN96, the 2nd International Workshop on the SPIN Verification System. DIMACS Series, American Mathematical Society, Providence, R.I., 1997.
Download: [PDF] [PS]Abstract: We discuss a translation of Message Sequence Charts (MSCs) into the language PROMELA (we call this translation an `{\em implementation}') that is consistent with the formal semantics we have previously defined for Message Flow Graphs and Message Sequence Charts, which handled the syntactic features with mathematical import from ITU-T recommendation Z.120. We report on experiments executing the PROMELA code using the XSPIN simulator and validator. In previous work we found that potential process {\em divergence} and {\em non-local choice} situations impose problems on implementations of MSCs, and we discuss how these impact our PROMELA translation and suggest solutions. Finally, we show how to model-check liveness requirements imposed on MSC specifications. We use the PROMELA models obtained from our implementation, describe how to use control state propositions based on these models, use Linear Time Temporal Logic formulas to specify the liveness properties, and demonstrate the use of XSPIN as a model checker for these properties. -
Hanêne Ben-Abdallah and Stefan Leue: Syntactic Detection of Process Divergence and non-Local Choice in Message Sequence Charts
, Volume 1217, Pages 259 - 274, Lecture Notes in Computer Science, Springer Verlag, 1997.
Download: [PDF] [PS]Abstract: Message Sequence Charts (MSCs) are increasingly used in software engineering methodologies and tools to capture, for instance, system requirements, test scenarios, and simulation traces. They have been standardized by ITU-T in Recommendation Z.120~\cite{ITU-T96}. However, various aspects of environment behavior remain underspecified in MSCs, e.g., the presence of resources for inter-process communication and the coordination of concurrent processes at points of control branching. Such underspecifications can result in ambiguities in an MSC specification and discrepancies between an MSC specification and its implementation. In this paper we characterize two consequences of harmful underspecifications: {\em process divergence} and {\em non-local branching choice}. We also present two syntax-based analysis algorithms that detect both problems. -
Hanêne Ben-Abdallah and Stefan Leue: Syntactic Detection of Process Divergence and non-Local Choice in Message Sequence Charts
, Proceedings of the Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems TACAS'97, 1997.
Download: [PDF] [PS]Abstract: Message Sequence Charts (MSCs) are increasingly used in software engineering methodologies and tools to capture, for instance, system requirements, test scenarios, and simulation traces. They have been standardized by ITU-T in Recommendation Z.120~\cite{ITU-T96}. However, various aspects of environment behavior remain underspecified in MSCs, e.g., the presence of resources for inter-process communication and the coordination of concurrent processes at points of control branching. Such underspecifications can result in ambiguities in an MSC specification and discrepancies between an MSC specification and its implementation. In this paper we characterize two consequences of harmful underspecifications: {\em process divergence} and {\em non-local branching choice}. We also present two syntax-based analysis algorithms that detect both problems. -
Hanêne Ben-Abdallah and Stefan Leue: Expressing and Analyzing Timing Constraints in Message Sequence Chart Specifications
, Technical Report 97-04, Dept. of Electrical and Computer Engineering, University of Waterloo, 1997.
Download: [PDF] [PS]Abstract: Message Sequence Charts (MSCs) are increasingly supported in software engineering tools and methodologies for communication systems. The last Z.120 standard extends MSCs with operators to organize them in a compositional, hierarchical fashion to describe systems with non-trivial sizes. When dealing with timing constraints, the standard is still evolving along with several proposals. This paper first reviews proposed extensions of MSCs to describe timing constraints. Secondly, the paper describes an analysis technique for timing consistency in iterating and branching MSC specifications. The analysis extends efficient current techniques for timing analysis of MSCs with no loops or branchings. Finally, we use an example to illustrate our analysis technique. -
Hanêne Ben-Abdallah and Stefan Leue: Timing Constraints in Message Sequence Chart Specifications , Formal Description Techniques X, Proceedings of the Tenth International Conference on Formal Description Techniques FORTE/PSTV'97, Chapman & Hall, 1997.
Download: [PDF] [PS]Abstract: When dealing with timing constraints, the Z.120 standard of Message Sequence Charts (MSCs) is still evolving along with several proposals. This paper first reviews proposed extensions of MSCs to describe timing constraints. Secondly, the paper describes an analysis technique for timing consistency in iterating and branching MSC specifications. The analysis extends efficient current techniques for timing analysis of MSCs with no loops nor branchings. Finally, the paper extends our syntactic analysis of process divergence to MSCs with timing constraints. -
Stefan Leue and Philippe Oechslin: On Parallelising and Optimising the Implementation of Communication Protocols
, Pages 55 - 70, IEEE/ACM Transactions on Networking 4 (1), 1996.
Download: [PDF] [PS]Abstract: We present a method for the automatic derivation of efficient protocol implementations from a formal specification. Optimised efficient protocol implementation has become an important issue in telecommunications systems engineering as recently network throughput has increased much faster than computer processing power. Efficiency will be attained by two measures. First, the inherent parallelism in protocol specifications will be exploited. Second, the order of execution of the operations involved in the processing of the protocol data will be allowed to differ from the order prescribed in the specification, thus allowing operations to be executed jointly and more efficiently. The method will be defined formally which is useful when implementing it as a tool. -
Stefan Leue and Philippe Oechslin: Opparim - A Method and Tool for Optimized Parallel Protocol Implementation
, Volume 5, Pages 125 - 143, Journal of High Speed Networks, 1996.
Download: [PDF] [PS]Abstract: We are introducing and discussing a method for the {\em op}timized and {\em par}allel {\em imp}lementation of protocols as well as a tool \opparim to apply the method automatically to the specification of a protocol. We present a study case representing an IP/TCP/FTP protocol stack specified in SDL. We show how \opparim generates dependence graphs from the specification and how it manipulates these graphs to allow for an optimised and possibly parallelised implementation. We then present a hardware architecture on which the protocol stack could be implemented and show the effects of our optimizations on the processing time of an incoming packet. Using two processing elements the optimised implementation executes in less than half the time of what we call a `faithful' implementation. -
Peter B. Ladkin and Stefan Leue: Implementing and Verifying Scenario-Based Specifications Using Promela/XSpin
, Participants Proc. of the Second SPIN Workshop, Rutgers University, New Brunswick, New Jersey, 1996.
Download: [PDF] [PS]Abstract: In previous work we defined a finite state semantics for Message Sequence Charts (MSCs) and suggested a translation of MSC specifications into Promela. We call this translation an implementation. In this paper we reconsider the implementation of MSCs and discuss what information needs to be added when implementing MSC specifications containing so-called non-local choices. Next, we show how to model-check liveness requirements imposed on MSC specifications. We use the Promela models obtained from our implementation, describe how to use control state propositions based on these models, use Linear Time Temporal Logic formulas to specify the liveness properties, and demonstrate the use of XSpin as a model checker for these properties. -
Hanêne Ben-Abdallah and Stefan Leue: Architecture of a Requirements and Design Tool Based on Message Sequence Charts
, Technical Report 96-13, Dept. of Electrical and Computer Engineering, University of Waterloo, 1996.
Download: [PDF] [PS]Abstract: Message Sequence Charts (MSCs) are increasingly supported in software engineering tools to capture system requirements, test scenarios, and simulation traces of reactive systems. The latest standard syntax of MSCs offers operations to compose MSCs in a hierarchical, iterating, and nondeterministic way. The various operators are a step towards increasing the applicability of MSCs to more than a trace language. However, current tools operate on MSCs that describe finite, deterministic behavior and none of them uses MSCs as a language for requirements specification and design of a system. In this paper, we propose an architecture for an MSC-based tool to support the requirements specification and design phases. The main functionalities of the tool are: an environment for the composition of system models through MSCs, syntactic and model-based analysis of an MSC model, and resolving resource related underspecifications in an MSC model. The proposed tool also supports synthesis mechanisms as a means to integrate our tool with available tools, e.g., the SPIN model-checker. In this paper, we also review the theoretical results we have currently developed towards realizing the proposed tool. -
Hanêne Ben-Abdallah and Stefan Leue: Syntactic Analysis of Message Sequence Chart Specifications
, Technical Report 96-12, Dept. of Electrical and Computer Engineering, University of Waterloo, 1996.
Download: [PDF] [PS]Abstract: Message Sequence Charts (MSCs) are gaining popularity in software engineering methods for concurrent and real-time systems. They are increasingly supported in software engineering tools to capture, for instance, system requirements, test scenarios, and simulation traces. MSCs have been standardized by ITU-T in Recommendation Z.120. However, various aspects of environment behavior remain underspecified in MSCs, e.g., the presence of resources for inter-process communication and the coordination of concurrent processes at points of control branching. Such underspecifications can result in ambiguities in an MSC specification and discrepancies between an MSC specification and its implementation. In this paper we characterize two consequences of harmful underspecifications: process divergence and non-local branching choice. We also present two syntax-based analysis algorithms that detect both problems. The syntactic characterization of these problems requires an MSC specification to be deadlock-free. Therefore, we also discuss deadlock detection in MSC specifications. -
Dieter Hogrefe and Stefan Leue (Ed.): Formal Description Techniques VII - Proceedings of the Seventh IFIP International Conference on Formal Description Techniques FORTE'94, Proceedings of the Seventh IFIP International Conference on Formal Description Techniques FORTE'94, Chapman & Hall, 1995.
Abstract: Not available. -
Stefan Leue: Specifying Real-Time Requirements for SDL Specifications - A Temporal Logic-Based Approach
, Proceedings of the Fifteenth International Symposium on Protocol Specification, Testing, and Verification PSTV'95, Chapmann & Hall, 1995.
Download: [PDF] [PS]Abstract: Many telecommunications systems engineers find it convenient to specify functional properties of their systems using state-transition based formal description techniques like SDL, Estelle or Message Sequence Charts (MSCs). However, the expressiveness of these techniques does not capture real-time requirements, an important class of Quality of Service (QoS) requirements in telecommunications systems design. In this paper we introduce a method for the integration of functional system properties given as SDL specifications with real-time temporal logic specifications. We call the resulting specifications {\em complementary specifications}. First we proof the inexpressiveness of SDL with respect to hard real-time bound requirements. Next we define a common model theoretic foundation which allows SDL specifications to be used jointly with temporal logic specifications. Then we give examples of real-time related delay bound, delay jitter, and isochronicity constraint QoS specifications. We also discuss how our method helps in the specification of various QoS mechanisms, like QoS negotiation, QoS monitoring and jitter compensation. We finally also point at the use of these specifications in a formal verification context. -
Peter B. Ladkin and Stefan Leue: Four Issues Concerning the Semantics of Message Flow Graphs
, Formal Description Techniques VII, Proc. of the Seventh IFIP International Conference on Formal Description Techniques FORTE'94, Chapman & Hall, 1995.
Download: [PDF] [PS]Abstract: We discuss four issues concerning the semantics of Message Flow Graphs (MFGs). MFGs are extensively used as pictures of message-passing behavior. One type of MFG, Message Sequence Chart (MSC) is ITU Standard Z.120. We require that a system described by an MFG has global states with respect to its message-passing behavior, with transitions between these states effected by atomic message-passing actions. Under this assumption, we argue (a) that the collection of global message states defined by an MFG is finite (whether for synchronous, asynchronous, or partially-asynchronous message-passing); (b) that the unrestricted use of `conditions' requires processes to keep control history variables of potentially unbounded size; (c) that allowing `crossing' messages of the same type implies certain properties of the environment that are neither explicit nor desirable, and (d) that liveness properties of MFGs are more easily expressed by temporal logic formulas over the control states than by B\"uchi acceptance conditions over the same set of states. -
Peter B. Ladkin and Stefan Leue: Comments on a Proposed Semantics for Basic Message Sequence Charts
, The Computer Journal 37 (9), 1995.
Download: [PDF] [PS]Abstract: Comments on a Proposed Semantics for Basic Message Sequence Charts, The Computer Journal, 37(9), January 1995. -
Peter B. Ladkin and Stefan Leue: Implementing Message Sequence Charts in Promela
, Proc. of the First SPIN Workshop, Proc. of the First SPIN Workshop, Montreal, Canada, 1995.
Download: [PDF] [PS]Abstract: We have previously defined a formal semantics for Message Flow Graphs and Message Sequence Charts, capturing most of the syntactic features contained in ITU-T recommendation Z.120. We discuss here a translation of MSCs into the language {\em Promela}, and report on experiments executing the Promela code using the {\em SPIN} simulator and validator. -
Peter B. Ladkin and Stefan Leue: Interpreting Message Flow Graphs
, Pages 473 - 509, Formal Aspects of Computing 7(5), 1995.
Download: [PDF] [PS]Abstract: We give a semantics for Message Flow Graphs (MFGs), which play the role for interprocess communication that Program Dependence Graphs play for control flow in parallel processes. MFGs have been used to analyse parallel code, and are closely related to Message Sequence Charts and Time Sequence Diagrams in telecommunications systems. Our requirements are firstly, to determine unambiguously exactly what execution traces are specified by an MFG, and secondly, to use a finite-state interpretation. Our methods function for both asynchronous and synchronous communications. From a set of MFGs, we define a transition system of global states, and from that a B\"uchi automaton by considering safety and liveness properties of the system. In order easily to describe liveness properties, we interpret the traces of the transition system as a model of Manna-Pnueli temporal logic. Finally, we describe the expressive power of MFGs by mimicking an arbitrary B\"uchi automaton by means of a set of MFGs. -
Stefan Leue: QoS Specification Based on SDL /MSC and Temporal Logic
, Proceedings of the Montreal Workshop on Multimedia Applications and Quality of Service Verification, Workshop on Multimedia Applications and Quality of Service Verification, Montreal, 1994.
Download: [PDF] [PS]Abstract: Many telecommunications systems engineers find it convenient to specify functional properties of their systems using state-transition based formal description techniques like SDL or Message Sequence Charts (MSCs). However, the expressiveness of these techniques does not capture Quality of Service (QoS) or Network Performance (Np) requirements because many of these on real-time bounds and probability constraints which these FDTs do not allow to express. However, suitably extended temporal logics allow for a description of these requirements. We introduce a method for the integration of functional system specifications given in SDL or MSC with temporal logic based specifications of QoS or Np requirements. We show how SDL and MSC specifications fit together with Temporal Logic specifications. Then we give examples of delay bound, delay jitter, isochronicity, stochastic reliability and stochastic delay bound constraint specifications. We discuss how our method helps in the specification of Np/QoS mapping problems, of QoS negotiation mechanisms, and of QoS monitoring. Finally we hint at methods for the formal verification of QoS and Np specifications. -
Stefan Leue and Philippe Oechslin: From SDL Specification to Optimized Parallel Protocol Implementations
, Pages 308 - 328, Proceedings of the Fourth International IFIP Workshop on Protocols for High Speed Networks, Chapman & Hall, 1994.
Download: [PDF] [PS]Abstract: We propose a formalized method that allows to automatically derive an optimized implementation from the formal specification of a protocol. Our method starts with the SDL specification of a protocol stack. We first derive a data and control flow dependence graph from each SDL process. Then, in order to perform cross-layer optimizations we combine the dependence graphs of different SDL processes. Next, we determine the common path through the multi-layer dependence graph. We then parallelize this graph wherever possible which yields a relaxed dependence graph. Based on this relaxed dependence graph we interpret different optimization concepts that have been suggested in the literature, in particular lazy messages and combination of data manipulation operations. Together with these interpretations the relaxed dependence graph can be be used as a foundation for a compile-time schedule on a sequential or parallel machine architecture. The formalization we provide allows our method to be embedded in a more comprehensive protocol engineering methodology. -
Stefan Leue and Philippe Oechslin: Formalizations and Algorithms for Optimized Parallel Protocol Implementation
, Proceedings of the IEEE International Conference on Network Protocols ICNP-94, IEEE Computer Scociety Press, Boston, Massachusetts, 1994.
Download: [PDF] [PS]Abstract: Not available. -
Stefan Leue and Philippe Oechslin: Enhancing Integrated Layer Processing using Common Case Anticipation and Data Dependence Analysis
, Proceedings of the First Internation Workshop on High Performance Protocol Architectures HIPPARCH '94, INRIA Sophia Antipolis, 1994.
Download: [PDF] [PS]Abstract: Not available. -
Peter B. Ladkin and Stefan Leue: What Do Message Sequence Charts Mean?
, Pages 301 - 316, Formal Description Techniques VI, IFIP Transactions C, Proc. of the 6th International Conference on Formal Description Techniques, 1994.
Download: [PDF] [PS]Abstract: We propose a semantics for Message Sequence Charts (MSCs). Our requirements are: to determine unambiguously which execution traces are allowed by an MSC; and to use a finite-state interpretation. Our semantics handles both synchronous and asynchronous communication. We define a global state automaton from an MSC, by first defining a transition system of global states, and from that a B\"uchi automaton. In using MSCs, properties of the environment and liveness properties of the MSC itself may be underspecified. We propose a method using temporal logic formulas to specify the required liveness properties. -
Stefan Leue: Methods and Semantics for Telecommunications Systems Engineering, Doctoral Dissertation, University of Berne, 1994.
Download: [PDF] [PS]Abstract: Not available. -
Peter B. Ladkin and Stefan Leue: Interpreting Message Sequence Charts (revised version), Technical Report TR 101, Dept. of Computing Science, University of Stirling, United Kingdom, 1993.
Abstract: Not available. -
Peter B. Ladkin and Stefan Leue: On the Semantics of Message Sequence Charts., Formale Methoden für Verteilte Systeme, K.G. Sauer-Verlag, München, 1993, ISBN: 3-598-22409-5.
Abstract: Not available. -
Stefan Leue and Philippe Oechslin: Optimization Techniques for Parallel Protocol Implementation
, Proceedings of the Fourth Workshop on Future Trends of Distributed Computing Systems, IEEE computer Society Press, 1993.
Download: [PDF] [PS]Abstract: Not available. -
Peter B. Ladkin and Stefan Leue: Interpreting Message Sequence Charts, Research Report RJ 8965, IBM Almaden Research Center, 1992.
Abstract: Not available.