Chair for Software and Systems Engineering
Prof. Dr. Stefan Leue

Login |
 
 

Publications

Diese Liste als BibTeX Datei herunterladen!

    2016

  • Georgiana Caltais, Stefan Leue and Mohammad Reza Mousavi : (De-)Composing Causality in Labeled Transition Systems. CREST: 1st Workshop on Causal Reasoning for Embedded and safety-critical Systems Technologies. (2016).
    Download: [pdf] [BibTex]

  • Georgiana Caltais, Florian Leitner-Fischer, Stefan Leue and Jannis Weiser : SysML to NuSMV Model Transformation via Object-Orientation. Sixth Workshop on Design, Modeling and Evaluation of Cyber Physical Systems. (2016).
    Download: [pdf] [BibTex]

  • Georgiana Caltais, Stefan Leue and Mohammad Reza Mousavi : On (De-)Composing Causality. 28th Nordic Workshop on Programming Theory. (2016).
    Download: [pdf] [BibTex]

  • Georgiana Caltais and Bertrand Meyer : On the Verification of SCOOP Programs. Science of Computer Programming. (2016).
    Download:  [BibTex] [www]

  • Florian Leitner-Fischer, Stefan Leue and Sirui Liu : Automated Freedom from Interference Analysis for Automotive Software. Proceedings of 4th International Workshop on Critical Automotive Applications: Robustness & Safety (CARS 2016), Gothenburg, Sweden (2016).
    Download: [pdf] [BibTex]

  • 2015

  • Florian Leitner-Fischer : Causality Checking of Safety-Critical Software and Systems. (2015).
    Download: [pdf] [BibTex]

  • Alina Bey and Christian Wienbruch : Intrinsic Network Properties Govern the Network Response to Repetitive Transcranial Magnetic Stimulation (rTMS) in a Neuronal Network Model Simulating the Effects of rTMS. Clinical Neurophysiology. 126 (8), e125-e126. (2015).
    Download: [pdf] [BibTex] [www] [doi]

  • Adrian Beer, Stephan Heidinger, Uwe Kühne, Florian Leitner-Fischer and Stefan Leue : Symbolic Causality Checking Using Bounded Model Checking. (2015).
    Download: [pdf] [BibTex]

  • 2014

  • Florian Leitner-Fischer and Stefan Leue : SpinCause: A Tool for Causality Checking. Proceedings of the International SPIN Symposium on Model Checking of Software (SPIN 2014), San Jose, CA, USA. (2014).
    Download: [pdf] [BibTex] [www]

  • Adrian Beer, Florian Leitner-Fischer and Stefan Leue : On the Relationship of Event Order Logic and Linear Temporal Logic. Technical Report soft-14-01, Chair for Software Engineering, University of Konstanz (2014).
    Download: [pdf] [BibTex] [www]

  • Adrian Beer, Uwe Kühne, Florian Leitner-Fischer and Stefan Leue : Towards Symbolic Causality Checking Using SAT-Solving. In Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2014). Dagstuhl, Germany. (2014).
    Download: [pdf] [BibTex] [www]

  • Adrian Beer, Uwe Kühne, Florian Leitner-Fischer, Stefan Leue, Rüdiger Prem : Symbolic Causality Checking Using SAT-Solving. Technical Report soft-14-02, Chair for Software Engineering, University of Konstanz (2014).
    Download: [pdf] [BibTex] [www]

    2013

  • Florian Leitner-Fischer and Stefan Leue: Probabilistic Fault Tree Synthesis using Causality Computation, International Journal of Critical Computer-Based Systems, Vol. 4, No. 2, pp.119–143, 2013.
    Abstract: X
    In recent years, several approaches to generate probabilistic counterexamples have been proposed. The interpretation of probabilistic counterexamples, however, continues to be problematic since they have to be represented as sets of paths, and the number of paths in this set may be very large. Fault trees (FTs) are a well-established industrial technique to represent causalities for possible system hazards resulting from system or system component failures. In this paper we extend the structural equation approach by Pearl and Halpern, which is based on Lewis counterfactuals, so that it can be applied to reason about causalities in a state-action trace model induced by a probabilistic counterexample. The causality relationships derived by the extended structural equation model are then mapped onto fault trees. We demonstrate the usefulness of our approach by applying it to a selection of case studies known from literature.
    Download: [PDF]


  • Florian Leitner-Fischer and Stefan Leue: Probabilistic Fault Tree Synthesis using Causality Computation, Technical Report soft-13-03, Chair for Software Engineering, University of Konstanz, 2013.
    Abstract: X
    In recent years, several approaches to generate probabilistic counterexamples have been proposed. The interpretation of probabilistic counterexamples, however, continues to be problematic since they have to be represented as sets of paths, and the number of paths in this set may be very large. Fault trees (FTs) are a well-established industrial technique to represent causalities for possible system hazards resulting from system or system component failures. In this paper we extend the structural equation approach by Pearl and Halpern, which is based on Lewis counterfactuals, so that it can be applied to reason about causalities in a state-action trace model induced by a probabilistic counterexample. The causality relationships derived by the extended structural equation model are then mapped onto fault trees. We demonstrate the usefulness of our approach by applying it to a selection of case studies known from literature.
    Download: [PDF]


  • Florian Leitner-Fischer and Stefan Leue: On the Synergy of Probabilistic Causality Computation and Causality Checking, In Model Checking Software - Proceedings of International SPIN Symposium on Model Checking of Software. Stony Brook, NY, USA. Lecture Notes in Computer Science Volume 7976, pp 246-263, Springer Verlag, 2013.
    Abstract: X
    In recent work on the safety analysis of systems we have shown how causal relationships amongst events can be algorithmically inferred from probabilistic counterexamples and subsequently be mapped to fault trees. The resulting fault trees were significantly smaller and hence easier to understand than the corresponding probabilistic counterexample, but still contain all information needed to discern the causes for the occurrence of a hazard. More recently we have developed an approach called Causality Checking which is integrated into the state-space exploration algorithms used for qualitative model checking and which is capable of computing causality relationships on-the-fly. The causality checking approach outperforms the probabilistic causality computation in terms of run-time and memory consumption, but can not provide a probabilistic measure. In this paper we combine the strengths of both approaches and propose an approach where the causal events are computed using causality checking and the probability computation can be limited to the causal events. We demonstrate the increase in performance of our approach using several case studies.
    Download: [PDF]


  • Stefan Leue and Mitra Tabaei Befrouei: Mining Sequential Patterns to Explain Concurrent Counterexamples., In Model Checking Software - Proceedings of International SPIN Symposium on Model Checking of Software. Stony Brook, NY, USA. Lecture Notes in Computer Science Volume 7976, pp 264-281, Springer Verlag, 2013.
    Abstract: X
    Concurrent systems are often modeled using an interleaving semantics. Since system designers tend to think sequentially, it is highly probable that they do not foresee some interleavings that their model encompasses. As a consequence, one of the main sources of failure in concurrent systems is unforeseen interleavings. In this paper, we devise an automated method for revealing unforeseen interleavings in the form of sequences of actions derived from counterexamples obtained by explicit state model checking. In order to extract such sequences we use a data mining technique called sequential pattern mining. Our method is based on contrasting the patterns of a set of counterexamples with the patterns of a set of correct traces that do not violate a desired property. We first argue that mining sequential patterns from the dataset of counterexamples fails due to the inherent complexity of the problem. We then propose a reduction technique designed to reduce the length of the execution traces in order to make the problem more tractable. We finally demonstrate the effectiveness of our approach by applying it to a number of sample case studies.
    Download: [PDF]


  • Adrian Beer, Todor Georgiev, Florian Leitner-Fischer and Stefan Leue: Model-Based Quantitative Safety Analysis of Matlab Simulink / Stateflow Models, In Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2013). Dagstuhl, Germany. 2013.
    Abstract: X
    In this paper we report on work in progress to extend the QuantUM approach to support the quantitative property analysis of Matlab Simulink / Stateflow models. We propose a translation of Simulink / Stateflow models to CTMCs which can be analyzed using the PRISM model checker inside the QuantUM tool. We also illustrate how the information needed to perform probabilistic analysis of dependability properties can be specified at the level of the Simulink / Stateflow model. We demonstrate the applicability of our approach using a case study taken from the MathWorks examples library.
  • Download: [PDF]

  • Adrian Beer, Uwe Kühne, Florian Leitner-Fischer, Stefan Leue and Rüdiger Prem: Quantitative Safety Analysis of Non-Deterministic System Architectures, Technical Report soft-13-02, Chair for Software Engineering, University of Konstanz, 2013.
    Abstract: X
    The QuantUM modeling framework and analysis tool, which allows for the modeling and analysis of quantitative aspects of system architectures modeled in UML / SysML, does not offer an adequate treatment of non-determinism. We present an semantics extension of the QuantUM approach so that non-determinism is supported with the aid of Markov Decision Processes. We show that the formal semantic interpretation of the UML / SysML models coincides with the code generation semantics for a widely used UML / SysML CASE tool. We evaluate the proposed approach by applying it to two industrial strength case studies, an Airport Surveillance Radar and an Airbag Control Unit.
    Download: [PDF]


  • Florian Leitner-Fischer and Stefan Leue: On the Synergy of Probabilistic Causality Computation and Causality Checking, Technical Report soft-13-01, Chair for Software Engineering, University of Konstanz, 2013.
    Abstract: X
    In recent work on the safety analysis of systems we have shown how causal relationships amongst events can be algorithmically inferred from probabilistic counterexamples and subsequently be mapped to fault trees. The resulting fault trees were significantly smaller and hence easier to understand than the corresponding probabilistic counterexample, but still contain all information needed to discern the causes for the occurrence of a hazard. More recently we have developed an approach called Causality Checking which is integrated into the state-space exploration algorithms used for qualitative model checking and which is capable of computing causality relationships on-the-fly. The causality checking approach outperforms the probabilistic causality computation in terms of run-time and memory consumption, but can not provide a probabilistic measure. In this paper we combine the strengths of both approaches and propose an approach where the causal events are computed using causality checking and the probability computation can be limited to the causal events. We demonstrate the increase in performance of our approach using several case studies.
    Download: [PDF]


  • F. Leitner-Fischer and S.Leue : Causality Checking for Complex System Models, In Proceedings of 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI2013),pp. 248-267, Lecture Notes in Computer Science, Volume 7737. Springer Verlag., 2013.
    Abstract: X
    We present an approach for the algorithmic computation of causalities in system models that we refer to as causality checking. We base our notion of causality on counterfactual reasoning, in particular using the structural equation model approach by Halpern and Pearl that we recently have extended to reason about computational models. In this paper we present a search-based on-the-fly approach that nicely integrates into finite state verification techniques, such as explicit-state model checking. We demonstrate the applicability of our approach using an industrial case study.
    Download: [PDF]


  • 2012

  • A. Bey, S. Leue, C. Wienbruch : A Neuronal Network Model for Simulating the Effects of Repetitive Transcranial Magnetic Stimulation on Local Field Potential Power Spectra, In PLOS ONE, 7(11): e49097, 2012.
    Abstract: X
    Repetitive transcranial magnetic stimulation (rTMS) holds promise as a non-invasive therapy for the treatment of neurological disorders such as depression, schizophrenia, tinnitus, and epilepsy. Complex interdependencies between stimulus duration, frequency and intensity obscure the exact effects of rTMS stimulation on neural activity in the cortex, making evaluation of and comparison between rTMS studies difficult. To explain the influence of rTMS on neural activity (e.g. in the motor cortex), we use a neuronal network model. The results demonstrate that the model adequately explains experimentally observed short term effects of rTMS on the band power in common frequency bands used in electroencephalography (EEG). We show that the equivalent local field potential (eLFP) band power depends on stimulation intensity rather than on stimulation frequency. Additionally, our model resolves contradictions in experiments.
    Download: [PDF]


  • Adrian Beer: Quantitative Analysis of Concurrent System Architectures, Master Thesis, University of Konstanz, 2012.
    Abstract: X
    Safety-critical software and systems development is subject to special dependability requirements. Early analysis of dependability during design and development phase is often a statutory condition for the approval of technical systems. In order to support the developers in verifying and analysing these systems the QuantUM tool was recently introduced. The UML model of the system can be annotated using the presented QuantUM-profile. Afterwards, QuantUM translates the annotated models into the input language of the probabilistic model checker PRISM, which is used as an analysis back-end. This thesis proposes an extension to the QuantUM method so that non-determinism is supported. Non-determinism is an essential paradigm when analysing concurrent system architectures. We introduce new translation rules into the QuantUM profile which are then used to transform UML or SysML models into locally uniform Continuous-Time Markov Decision Processes. Since there are no efficient model checking algorithms for CTMDPs, a discretization technique is applied to convert the CTMDP into discrete-time MDPs. The new approach is applied to two case studies, an Airport Surveillance Radar and an Airbag Control Unit.
    Download: [PDF]


  • Stefan Leue and Mitra Tabaei Befrouei: Counterexample Explanation by Anomaly Detection, Pages 24-42, Proceedings of 19th International SPIN Workshop on Model Checking of Software (SPIN '12), Lecture Notes in Computer Science, Volume 7385. Springer Verlag., 2012.
    Abstract: X
    Since counterexamples generated by model checking tools are only symptoms of faults in the model, a significant amount of manual work is required in order to locate the fault that is the root cause for the presence of counterexamples in the model. In this paper, we propose an automated method for explaining counterexamples that are symptoms of the occurrence of deadlocks in concurrent systems. Our method is based on an analysis of a set of counterexamples that can be generated by a model checking tool such as SPIN. By comparing the set of counterexamples with the set of correct traces that never deadlock, a number of sequences of actions are extracted that aid the model designer in locating the cause of the occurrence of a deadlock. We first argue that the obvious approach to extract such sequences which is by sequential pattern mining and by contrasting patterns that are typical for the deadlocking counterexample traces but not typical for non-deadlocking traces, fails due to the inherent complexity of the problem. We then propose to extract substrings of specific length that only occur in the set of counterexamples for explaining the occurrence of deadlocks. We use a number of case studies to show the effectiveness of our approach and to compare it with an alternative approach to the counterexample explanation problem.
    Download: [PDF]


  • Florian Leitner-Fischer and Stefan Leue: Causality Checking for Complex System Models, Technical Report soft-12-02, Chair for Software Engineering, University of Konstanz. 2012.
    Abstract: X
    With the increasing growth of the size and complexity of modern safety-critical systems, the demand for model based engineering methods that both help in architecting such systems and to asses their safety and correctness becomes increasingly obvious. Causality checking is an automated method for formal causality analysis of system models and system execution traces. In this paper we report on work in progress towards an on-the-fly approach for causality checking of system models. We also sketch how this approach can be applied in model-based system analysis when assessing the system's functional correctness.
    Download: [PDF]


  • Adrian Beer, Uwe Kühne, Florian Leitner-Fischer, Stefan Leue and Rüdiger Prem: Analysis of an Airport Surveillance Radar using the QuantUM approach, Technical Report soft-12-01, Chair for Software Engineering, University of Konstanz. 2012.
    Abstract: X
    We report on the modeling and formal analysis of reliability requirements in the context of an Airport Surveillance Radar system using SysML and probabilistic model checking. The system is modeled using the QuantUM modeling tool which uses the PRISM model checker as an analysis back-end. We illustrate how a complex system architecture can be modeled, what challenges have to be addressed when performing the automated property verification, and to what extent the presented automated analysis method can support the system engineering. We expect that the use of these methods will also have a strong impact on the certification process in future.
    Download: [PDF]


  • Florian Leitner-Fischer and Stefan Leue: Towards Causality Checking for Complex System Models, In Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2012). Dagstuhl, Germany. 2012.
    Abstract: X
    With the increasing growth of the size and complexity of modern safety-critical systems, the demand for model based engineering methods that both help in architecting such systems and to asses their safety and correctness becomes increasingly obvious. Causality checking is an automated method for formal causality analysis of system models and system execution traces. In this paper we report on work in progress towards an on-the-fly approach for causality checking of system models. We also sketch how this approach can be applied in model-based system analysis when assessing the system's functional correctness.
    Download: [PDF]
  • 2011

  • Husain Aljazzar and Stefan Leue: K*: A Heuristic Search Algorithm for Finding the k Shortest Paths, Artificial Intelligence, Volume 175, Number 18, December 2011 2011.
    Abstract: X
    We present a directed search algorithm, called K$^*$, for finding the $k$ shortest paths between a designated pair of vertices in a given directed weighted graph. K$^*$ has two advantages compared to current k-shortest-paths algorithms. First, K$^*$ operates 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$^*$ can be guided using heuristic functions. %This leads to significant improvements in the %memory and runtime demands for many practical problem instances. We prove the correctness of K$^*$ and determine its asymptotic worst-case complexity when using a consistent heuristics to be the same as the state of the art, $\bigo(m + n \log n + k)$, with respect to both runtime and space, where $n$ is the number of vertices and $m$ is the number of edges of the graph. We present an experimental evaluation of K$^*$ by applying it to route planning problems as well as counterexample generation for stochastic model checking. The experimental results illustrate that due to the use of heuristic, on-the-fly search K$^*$ can use less time and memory compared to the most efficient k-shortest-paths algorithms known so far.
    Download: [PDF]


  • Matthias Kuntz, Florian Leitner-Fischer and Stefan Leue: From Probabilistic Counterexamples via Causality to Fault Trees, In Proceedings of 30th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2011), 2011.
    Abstract: X
    Probabilistic Model Checking is an established technique used in the dependability analysis of safety-critical systems. In recent years, several approaches to generate probabilistic counterexamples have been proposed. The interpretation of stochastic counterexamples, however, continues to be problematic since they have to be represented as sets of paths, and the number of paths in this set may be very large. Fault trees (FTs) are a well-established industrial technique to represent causalities for possible system hazards resulting from system or system component failures. In this paper we suggest a method to automatically derive FTs from counterexamples, including a mapping of the probability information onto the FT. We extend the structural equation approach by Pearl and Halpern, which is based on Lewis counterfactuals, so that it serves as a justification for the causality that our proposed FT derivation rules imply. The synthesized FTs provide the user with a concise and compact representation of the causes of potential system failures, together with their respective probabilities. We demonstrate the usefulness of our approach by applying it to a selection of industrial size case studies.
    Download: [PDF]


  • Husain Aljazzar, Florian Leitner-Fischer, Stefan Leue and Dimitar Simeonov: DiPro - A Tool for Probabilistic Counterexample Generation, In Proceedings of 18th International SPIN Workshop on Model Checking of Software (SPIN 2011), 2011.
    Abstract: X
    The computation of counterexamples for probabilistic model checking has been an area of active research over the past years. In spite of the achieved theoretical results in this field, there is no freely available tool that allows for the computation and representation of probabilistic counterexamples. We present an open source tool called DiPro that can be used with the PRISM and MRMC probabilistic model checkers. It allows for the computation of probabilistic counterexamples for discrete time Markov chains (DTMCs), continuous time Markov chains (CTMCs) and Markov decision processes (MDPs). The computed counterexamples can be rendered graphically.
    Download: [PDF]


  • Dominic Lehle: Quantitative Safety Analysis of SysML Models, Bachelor Thesis, University of Konstanz 2011.
    Abstract: X
    Throughout the implementation of safety-critical systems the decision which requirements should be prioritized have to be balanced. It has been often ignored that many failures of a system could have been addressed in early design processes. Despite the lack of well-engineered methods for safety analysis, the costs and complexity often even keep industry giants away from the safety analysis in early stages of the development. Another criteria is that immersed knowledge is required and not often found in industrial methods. In QuantUM, a successful approach of Florian Leitner-Fischer to bridge this gap and improve the integration of quantitative safety analysis methods into the development process, all inputs needed for this type of analysis can be specified at the level of an UML model. However the gap still exists for models which are not principally software-systems. The SysML is a language based on UML and is an established standard in modeling complex and embedded systems in the industry today. Due to the fact that UML includes, in the manner of speaking, the basic principles for SysML, it is convenient to apply and adjust an existent approach in order to bridge the gap in systems engineering. As a result we propose a profile for SysML to enable the specification of all inputs needed for quantitative safety analysis in the early development process, and extend the functionality of the existent software on the level of SysML.
    Download: [PDF]


  • Alina Bey and Stefan Leue: Modeling and Analyzing Spike Timing Dependent Plasticity with Linear Hybrid Automata, Technical Report soft-11-03, Chair for Software Engineering, University of Konstanz. 2011.
    Abstract: X
    We propose a model for synaptic plasticity according to the Spike Timing Dependent Plasticity (STDP) theory using Linear Hybrid Au- tomata (LHA). We first present a compositional LHA model in which each component corresponds to some process in STDP. We then ab- stract this model into a monolithic LHA model in order to enable formal analysis using hybrid model checking. We discuss how the avail- ability of an LHA model as well as its formal analysis using the tool PHAVer can support a better understanding of the dynamics of STDP.
    Download: [PDF]


  • Matthias Kuntz, Florian Leitner-Fischer and Stefan Leue: From Probabilistic Counterexamples via Causality to Fault Trees, Technical Report soft-11-02, Chair for Software Engineering, University of Konstanz. 2011.
    Abstract: X
    Probabilistic Model Checking is an established technique used in the dependability analysis of safety-critical systems. In recent years, several approaches to generate probabilistic counterexamples have been proposed. The interpretation of stochastic counterexamples, however, continues to be problematic since they have to be represented as sets of paths, and the number of paths in this set may be very large. Fault trees (FTs) are a well-established industrial technique to represent causalities for possible system hazards resulting from system or system component failures. In this paper we suggest a method to automatically derive FTs from counterexamples, including a mapping of the probability information onto the FT. We extend the structural equation approach by Pearl and Halpern, which is based on Lewis counterfactuals, so that it serves as a justification for the causality that our proposed FT derivation rules imply. The synthesized FTs provide the user with a concise and compact representation of the causes of potential system failures, together with their respective probabilities. We demonstrate the usefulness of our approach by applying it to a selection of industrial size case studies.
    Download: [PDF]


  • Florian Leitner-Fischer, Stefan Leue: The QuantUM Approach in the Context of the ISO Standard 26262 for Automotive Systems (Extended Abstract), Technical Report soft-11-01, Chair for Software Engineering, University of Konstanz. 2011.
    Abstract: X
    The forthcoming standard ISO 26262 defines processes and techniques in support of a safe design and implementation of automotive systems. We comment on the recommendations that this standard provides with respect to the use of semi-formal and formal methods, including formal verification, during various stages of the proposed safety process. We illustrate how the QuantUM method and tool that we have developed in order to open UML-type system architecture models to formal analysis using stochastic model checking can be applied in support of the safety requirements imposed by the standard.
    Download: [PDF]


  • Matthias Kuntz, Florian Leitner-Fischer, Stefan Leue and Bernd Reh: Challenges in the Modelling and Quantitative Analysis of Safety-Critical Automotive Systems, Presentation at ROCKS workshop (ROCKS 2011). Saarbrücken, Germany. 2011.
    Abstract: X
    In modern cars safety-critical and safety-relevant embedded hard- and software systems are ubiquitous. These systems include systems for active and passive safety such as driving dynamics, braking assistance, and passenger restraint systems such as active control retractors and airbag systems. These systems help to protect car occupants and other road users from potentially fatal injuries. But, the affectees have to rely on the correct functioning of the safety systems. To assure this, a systematic system development begining at the architectural level down to hard- and software implementation is required by the upcoming international norm for functional safety of road vehicles, ISO26262. A norm-compliant development cycle has to prove that the system under consideration satisfies both qualitative and quantitative target measures. Depending on the safety-criticality, the automotive safety integrity level (ASIL) ISO26262 puts tight limits on failure rates for automotive systems. In this work, we will show by means of two different approaches how probabilistic modelling and analysis for the system and hardware level can help to systematically develop automotive safety-critical systems in a way that helps to safe both development time and costs. We will present the quantitative, i.e., probabilistic extension of UML, QuantUM, that can be used to assess the dependability of an automotive system. Secondly, we present a method to use dynamic fault trees to represent probabilistic counter examples to give the system developer a concise overview on desing flaws in case the required ASIL cannot be reached. We will demonstrate the feasibility of the presented approaches by means of an airbag case study, that is derived from a real-world TRW application project.
    Download: [PDF]


  • Florian Leitner-Fischer and Stefan Leue: QuantUM: Quantitative Safety Analysis of UML Models, In Proceedings of Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011). Saarbrücken, Germany. 2011.
    Abstract: X
    When developing a safety-critical system it is essential to obtain an assessment of different design alternatives. In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of available formal quantitative analysis methods it is still difficult for software and system architects to integrate these techniques into their every day work. This is mainly due to the lack of methods that can be directly applied to architecture level models, for instance given as UML diagrams. Also, it is necessary that the description methods used do not require a profound knowledge of formal methods. Our approach bridges this gap and improves the integration of quantitative safety analysis methods into the development process. All inputs of the analysis are specified at the level of a UML model. This model is then automatically translated into the analysis model, and the results of the analysis are consequently represented on the level of the UML model. Thus the analysis model and the formal methods used during the analysis are hidden from the user. We illustrate the usefulness of our approach using an industrial strength case study.
    Download: [PDF]


  • Florian Leitner-Fischer and Stefan Leue: Quantitative Analysis of UML Models, In Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2011). Dagstuhl, Germany. 2011.
    Abstract: X
    When developing a safety-critical system it is essential to obtain an assessment of different design alternatives. In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of available formal quantitative analysis methods it is still difficult for software and system architects to integrate these techniques into their every day work. This is mainly due to the lack of methods that can be directly applied to architecture level models, for instance given as UML diagrams. Our approach bridges this gap and improves the integration of quantitative safety analysis methods into the development process. We propose a UML profile that allows for the specification of all inputs needed for the analysis at the level of a UML model. The QuantUM tool which we have developed, automatically translates an UML model into an analysis model. Furthermore, the results gained from the analysis are lifted to the level of the UML specification or other high-level formalism to further facilitate the process. Thus the analysis model and the formal methods used during the analysis are hidden from the user.
    Download: [PDF]


  • Stefan Leue and Wei Wei: Integer Linear Programming Based Property Checking for Asynchronous Reactive Systems, IEEE Transactions on Software Engineering, vol. 99, 2011.
    Abstract: X
    Asynchronous reactive systems form the basis of a wide range of software systems, for instance in the telecommunications domain. It is highly desirable to rigorously show that these systems are correctly designed. However, traditional formal approaches to the verification of these systems are often difficult because asynchronous reactive systems usually possess extremely large or even infinite state spaces. We propose an Integer Linear Program (ILP) solving based property checking framework that concentrates on the local analysis of the cyclic behavior of each individual component of a system. We apply our framework to the checking of the buffer boundedness and livelock freedom properties, both of which are undecidable for asynchronous reactive systems with an infinite state space. We illustrate the application of the proposed checking methods to Promela, the input language of the SPIN model checker. While the precision of our framework remains an issue, we propose a counterexample guided abstraction refinement procedure based on the discovery of dependencies among control flow cycles. We have implemented prototype tools with which we obtained promising experimental results on real life system models.
    Download: [PDF]
  • 2010

  • Florian Leitner-Fischer: Quantitative Safety Analysis of UML Models, Master Thesis, University of Konstanz, 2010.
    Abstract: X
    When developing a safety-critical system it is essential to obtain an assessment of different design alternatives. In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of available formal quantitative analysis methods it is still difficult for software and system architects to integrate these techniques into their every day work. This is mainly due to the lack of methods that can be directly applied to architecture level models, for instance given as UML diagrams. Another obstacle is, that the methods often require a profound knowledge of formal methods, which can rarely be found in industrial practice. Our approach bridges this gap and improves the integration of quantitative safety analysis methods into the development process. We propose a UML profile that allows for the specification of all inputs needed for the analysis at the level of a UML model. The QuantUM tool which we have developed, automatically translates an UML model into an analysis model. Furthermore, the results gained from the analysis are lifted to the level of the UML specification or other high-level formalism to further facilitate the process. Thus the analysis model and the formal methods used during the analysis are hidden from the user.
    Download: [PDF]


  • Boudewijn R. Haverkort, Matthias Kuntz, Florian Leitner-Fischer, Anne Remke and Stephan Roolvink: Probabilistic verification of Architectural software models using SoftArc and Prism, In: Proceedings of the ESREL 2010 Annual Conference, 5-9 Sept 2010, Greece, Rhodos. pp. 852-860. Taylor & Francis. ISBN 978-0-415-60427-7, 2010.
    Abstract: X
    In this paper we will describe the SoftArc approach. With the SoftArc approach it is possible to model and analyse safety-critical embedded and distributed systems that consist of both hard- and software. We are going to present the SoftArc modelling language, its syntax and semantics. The semantics of the SoftArc modelling language is defined in terms of stochastic reactive modules. We will show how important measures of interest for probabilistic dependability analysis like availability, unavailability, and survivability, i.e., the possibility of a system to recover into an operational mode in the presence of catastrophic events can be formulated and automatically analysed using the SoftArc approach. We will briefly explain how probabilistic FMEA can be done using SoftArc. We will demonstrate the feasibility of our approach by means of three case studies, that involve hard- and software elements. First, we are presenting two industrial case studies from the automotive industry. We will analyse the non volatile random access manager (NVRAM) from the AUTOSAR open system architecture, second we will do a probabilistic FMEA of an airbag control unit. Finally, we are going to present the survivability analysis of a simplified version of the Google file system.
    Download: [PDF]


  • B.R. Haverkort, M. Kuntz, A. Remke, S. Roolvink: Formal Performability Evaluation of Architectural Models of Critical Infrastructures., In: Proceedings of the ESREL 2010 Annual Conference, 5-9 Sept 2010, Greece, Rhodos. pp. 27-34. Taylor & Francis Group. ISBN 978-0-415-60427-7, 2010.
    Abstract: X
    In this paper, we introduce MIOA, a stochastic process algebra-like specification language with finite-domain datatypes, as well as the logic intSPDL, and its model checking algorithms. MIOA which stands for Markovian input/output automata language is an extension of Lynch’s input/output automata with Markovian timed transitions. MIOA can serve both as a fully fledged “stand-alone” specification language and as the semantic model for the architectural dependability description language Arcade. The logic intSPDL is an extension of the stochastic logic SPDL, designed to deal with the specialties of MIOA. In the context of Arcade, intSPDL can be seen as the semantic model of abstract and complex dependability measures that can be defined in the Arcade framework. We define syntax and semantics of both MIOA and intSPDL, and present application examples of MIOA and intSPDL in the realm of dependability modelling with Arcade.
    Download: [PDF]


  • B.R. Haverkort, M. Kuntz, A. Remke, S. Roolvink, M.I.A. Stoelinga: Evaluating Repair Strategies for a Water-Treatment Facility using Arcade, In: 2010 IEEE/IFIP International Conference on Dependable Systems & Networks (DSN), 28 June - 1 July 2010, Chicago, IL, USA. pp. 419-424. IEEE Computer Society Press. ISBN 978-1-4244-7499-8, 2010.
    Abstract: X
    The performance and dependability of critical infrastructures, such as water-treatment facilities is essential. In this paper we use various performance and dependability measures to analyze a simplified model of a water treatment facility. Building on the existing architectural framework Arcade a model is derived in XML format and then automatically mapped to the model checker PRISM. Using the stochastic model checking capabilities that PRISM offers, we compare different repair strategies, with respect to their costs, system reliability, availability and survivability. For this case study we conclude that using non-preemtive priority scheduling with additional repair crews is the best choice with respect to performance, dependability and costs
    Download: [PDF]


  • Matthias Kuntz, Stefan Leue and Christoph Scheben: Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs, Third International Workshop on Invariant Generation (WING 2010), 2010.
    Abstract: X
    Currently, no approaches are known that allow for non-termination proofs of concurrent programs which account for asynchronous communication via FIFO message queues. Those programs may be written in high-level languages such as Java or Promela. We present a first approach to prove non- termination for such programs. In addition to integers, the programs that we consider may contain queues as data structures. We present a representation of queues and the operations on them in the domain of integers, and generate invariants that help us prove non-termination of selected control flow loops using a theorem proving approach. We illustrate this approach by applying a prototype tool implementation to a number of case studies.
    Download: [PDF]


  • Husain Aljazzar and Stefan Leue: K*: Heuristics-Guided, On-the-Fly k Shortest Paths Search, Accepted for publication at Sixth Workshop on Model Checking and Artificial Intelligence (MoChArt 2010), 2010.
    Abstract: X
    We present a search algorithm, called K*, for finding the k shortest paths (KSP) between a designated pair of vertices in a given directed weighted graph. As a directed algorithm, K* has two advantages compared to current KSP algorithms. 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* can be guided using heuristic functions. We prove the correctness of K* and determine its asymptotic worst-case complexity as O(m + n log n + k) with respect to both runtime and space, where n is the number of vertices and m is the number of edges of the graph. We present an experimental evaluation of K* by applying it to route planning problems. The experimental results illustrate the favorable performance of K* compared to the most efficient k-shortest-paths algorithms known so far. In other work it has been shown that K* can be used to efficiently compute counterexamples for stochastic model checking.
    Download: [PDF]


  • Husain Aljazzar and Matthias Kuntz and Florian Leitner-Fischer and Stefan Leue: Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative Evaluation, In: Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems, 2010.
    Abstract: X
    The generation of counterexamples for probabilistic model checking has been an area of active research over the past five years. Tangible outcome of this research are novel directed and heuristic algorithms for efficient generation of probabilistic counterexamples, such as $K^{*}$ and XBF. In this paper we present an empirical evaluation of the efficiency of these algorithms and the well-known Eppstein's algorithm. We will also evaluate the effect of optimizations applied to Eppstein, $K^{*}$ and XBF. Additionally, we will show, how information produced during model checking can be used to guide the search for counterexamples. This is a first step towards automatically generating heuristic functions. The experimental evaluation of the various algorithms is done by applying them to one case study, known from the literature on probabilistic model checking and one case study taken from the automotive industry.
    Download: [PDF]


  • 2009

  • Husain Aljazzar: Directed Diagnostics of System Dependability Models , Doctoral Dissertation, University of Konstanz, 2009.
    Abstract: X
    Model checking, as a formal verification technique, aims primarily at proving the correctness of systems. Nevertheless, model checking has also been extensively used as a debugging technique to aid developers in locating and fixing errors when the model violates a desired property. Thus, the ability to provide diagnostic information, that facilitates debugging, dictates the usability of model checking techniques in practice. Counterexamples are the prime example of such diagnostic information. A counterexample is in general a piece of information which attests the property violation and which can be used for explaining the causal factors of the property violation. Stochastic model checking extends conventional model checking with the verification of quantitative performance and dependability requirements. The core of stochastic model checkers is a set of efficient numerical algorithms which compute the probabilities that determine the satisfaction or violation of a given property. Due to the numerical nature of these algorithms, stochastic model checkers do not provide counterexamples. Within our research in this field we succeeded in extending stochastic model checking to include the possibility of counterexample generation. We introduced the notion of counterexamples into stochastic model checking and devised the first methods for the generation and analysis of counterexamples. We begin this dissertation with an introduction into stochastic model checking followed by a study of counterexamples in stochastic model checking where we give a formal definition for counterexamples for common stochastic models. We also discuss the characteristics of informative counterexamples in this context and present a variety of novel methods for the generation of informative counterexamples. Our methods are based on heuristics-guided search algorithms, also called directed search algorithms. We investigate these methods in different settings and examine their advantages and disadvantages. We also investigate their applicability to models with real-life complexity. We present extensive experiments using significant case studies. These experiments demonstrate the efficiency and scalability of our methods. They also show that the counterexamples produced by our methods are informative and useful for debugging. Counterexamples in stochastic model checking, as we will show in this dissertation, are very complex. Thus, analysing them for the purpose of debugging is a very challenging task for human users. We propose the first method which aids engineers in analysing counterexample in stochastic model checking. Our method employs interactive visualisation techniques which aim at determining the causal factors of property violations. A significant contribution of our research on counterexample generation is the development of a novel directed search algorithm K* for solving the k-shortest-paths problem. This is the problem of finding k shortest paths form a start to a target node in a weighted directed graph for an arbitrary natural number k. The k-shortest-paths problem is a general problem with a wide range of applications. K* scales to very large graphs compared to classical k-shortest-paths algorithms. We demonstrate the advantage of K* by applying it to route planning in the US road map.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • Bahareh Badban, Stefan Leue, Jan-Georg Smaus: Automated Predicate Abstraction for Real-Time Models, INFINITY 2009, 11th International Workshop on Verification of Infinite-State Systems, 2009.
    Abstract: X
    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.
    Download: [PDF]


  • 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: X
    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.
    Download: [PDF]


  • Bahareh Badban: A Term Rewriting Technique for Decision Graphs, in the International Workshop on Computing with Terms and Graphs (TERMGRAPH), 2009.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • Christian Dax, Felix Klaedtke and Stefan Leue: Specification Languages for Stutter-Invariant Regular Properties, In Proceedings of Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Lecture Notes in Computer Science, Springer Verlag, 2009.
    Abstract: X
    We present speci cation languages that naturally capture exactly the regular and w-regular properties that are stutter invariant. Our speci cation languages are variants of the classical regular expres- sions and of the core of PSL, a temporal logic, which is widely used in industry and which extends the classical linear-time temporal logic LTL by semi-extended regular expressions.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 2008

  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • Bahareh Badban: Culling predicates for the Verification of Real-Time Models, Technical Report soft-08-06, Chair for Software Engineering, University of Konstanz, 2008.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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).
    Download: [PDF]


  • 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: X
    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.
    Abstract: X
    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.
    Download: [PDF]


  • Wei Wei: Incomplete Property Checking for Asynchronous Reactive Systems, Doctoral Dissertation, University of Konstanz, 2008.
    Abstract: X
    Not available.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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: X
    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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 2007

  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 2006

  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 2005

  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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: X
    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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 2004

  • 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.
    Abstract: X
    Not available.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 2003

  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 2002

  • 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: X
    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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 2001

  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 2000

  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 1999

  • 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: X
    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: X
    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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 1998

  • 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: X
    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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 1997

  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • Stefan Fischer and Stefan Leue: Formal Methods for Broadband and Multimedia Systems , Computer Networks and ISDN Systems, 1997.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 1996

  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 1995

  • 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: X
    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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • Peter B. Ladkin and Stefan Leue: Comments on a Proposed Semantics for Basic Message Sequence Charts , The Computer Journal 37 (9), 1995.
    Abstract: X
    Comments on a Proposed Semantics for Basic Message Sequence Charts, The Computer Journal, 37(9), January 1995.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • Peter B. Ladkin and Stefan Leue: Interpreting Message Flow Graphs , Pages 473 - 509, Formal Aspects of Computing 7(5), 1995.
    Abstract: X
    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.
    Download: [PDF]


  • 1994

  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    Not available.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    Not available.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • Stefan Leue: Methods and Semantics for Telecommunications Systems Engineering, Doctoral Dissertation, University of Berne, 1994.
    Abstract: X
    Not available.
    Download: [PDF] [PS]


  • 1993

  • 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: X
    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: X
    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.
    Abstract: X
    Not available.
    Download: [PDF] [PS]


  • 1992

  • Peter B. Ladkin and Stefan Leue: Interpreting Message Sequence Charts, Research Report RJ 8965, IBM Almaden Research Center, 1992.
    Abstract: X
    Not available.


    2013

  • Florian Leitner-Fischer and Stefan Leue: Probabilistic Fault Tree Synthesis using Causality Computation, International Journal of Critical Computer-Based Systems, Vol. 4, No. 2, pp.119–143, 2013.
    Abstract: X
    In recent years, several approaches to generate probabilistic counterexamples have been proposed. The interpretation of probabilistic counterexamples, however, continues to be problematic since they have to be represented as sets of paths, and the number of paths in this set may be very large. Fault trees (FTs) are a well-established industrial technique to represent causalities for possible system hazards resulting from system or system component failures. In this paper we extend the structural equation approach by Pearl and Halpern, which is based on Lewis counterfactuals, so that it can be applied to reason about causalities in a state-action trace model induced by a probabilistic counterexample. The causality relationships derived by the extended structural equation model are then mapped onto fault trees. We demonstrate the usefulness of our approach by applying it to a selection of case studies known from literature.
    Download: [PDF]


  • Florian Leitner-Fischer and Stefan Leue: Probabilistic Fault Tree Synthesis using Causality Computation, Technical Report soft-13-03, Chair for Software Engineering, University of Konstanz, 2013.
    Abstract: X
    In recent years, several approaches to generate probabilistic counterexamples have been proposed. The interpretation of probabilistic counterexamples, however, continues to be problematic since they have to be represented as sets of paths, and the number of paths in this set may be very large. Fault trees (FTs) are a well-established industrial technique to represent causalities for possible system hazards resulting from system or system component failures. In this paper we extend the structural equation approach by Pearl and Halpern, which is based on Lewis counterfactuals, so that it can be applied to reason about causalities in a state-action trace model induced by a probabilistic counterexample. The causality relationships derived by the extended structural equation model are then mapped onto fault trees. We demonstrate the usefulness of our approach by applying it to a selection of case studies known from literature.
    Download: [PDF]


  • Florian Leitner-Fischer and Stefan Leue: On the Synergy of Probabilistic Causality Computation and Causality Checking, In Model Checking Software - Proceedings of International SPIN Symposium on Model Checking of Software. Stony Brook, NY, USA. Lecture Notes in Computer Science Volume 7976, pp 246-263, Springer Verlag, 2013.
    Abstract: X
    In recent work on the safety analysis of systems we have shown how causal relationships amongst events can be algorithmically inferred from probabilistic counterexamples and subsequently be mapped to fault trees. The resulting fault trees were significantly smaller and hence easier to understand than the corresponding probabilistic counterexample, but still contain all information needed to discern the causes for the occurrence of a hazard. More recently we have developed an approach called Causality Checking which is integrated into the state-space exploration algorithms used for qualitative model checking and which is capable of computing causality relationships on-the-fly. The causality checking approach outperforms the probabilistic causality computation in terms of run-time and memory consumption, but can not provide a probabilistic measure. In this paper we combine the strengths of both approaches and propose an approach where the causal events are computed using causality checking and the probability computation can be limited to the causal events. We demonstrate the increase in performance of our approach using several case studies.
    Download: [PDF]


  • Stefan Leue and Mitra Tabaei Befrouei: Mining Sequential Patterns to Explain Concurrent Counterexamples., In Model Checking Software - Proceedings of International SPIN Symposium on Model Checking of Software. Stony Brook, NY, USA. Lecture Notes in Computer Science Volume 7976, pp 264-281, Springer Verlag, 2013.
    Abstract: X
    Concurrent systems are often modeled using an interleaving semantics. Since system designers tend to think sequentially, it is highly probable that they do not foresee some interleavings that their model encompasses. As a consequence, one of the main sources of failure in concurrent systems is unforeseen interleavings. In this paper, we devise an automated method for revealing unforeseen interleavings in the form of sequences of actions derived from counterexamples obtained by explicit state model checking. In order to extract such sequences we use a data mining technique called sequential pattern mining. Our method is based on contrasting the patterns of a set of counterexamples with the patterns of a set of correct traces that do not violate a desired property. We first argue that mining sequential patterns from the dataset of counterexamples fails due to the inherent complexity of the problem. We then propose a reduction technique designed to reduce the length of the execution traces in order to make the problem more tractable. We finally demonstrate the effectiveness of our approach by applying it to a number of sample case studies.
    Download: [PDF]


  • Adrian Beer, Todor Georgiev, Florian Leitner-Fischer and Stefan Leue: Model-Based Quantitative Safety Analysis of Matlab Simulink / Stateflow Models, In Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2013). Dagstuhl, Germany. 2013.
    Abstract: X
    In this paper we report on work in progress to extend the QuantUM approach to support the quantitative property analysis of Matlab Simulink / Stateflow models. We propose a translation of Simulink / Stateflow models to CTMCs which can be analyzed using the PRISM model checker inside the QuantUM tool. We also illustrate how the information needed to perform probabilistic analysis of dependability properties can be specified at the level of the Simulink / Stateflow model. We demonstrate the applicability of our approach using a case study taken from the MathWorks examples library.
  • Download: [PDF]

  • Adrian Beer, Uwe Kühne, Florian Leitner-Fischer, Stefan Leue and Rüdiger Prem: Quantitative Safety Analysis of Non-Deterministic System Architectures, Technical Report soft-13-02, Chair for Software Engineering, University of Konstanz, 2013.
    Abstract: X
    The QuantUM modeling framework and analysis tool, which allows for the modeling and analysis of quantitative aspects of system architectures modeled in UML / SysML, does not offer an adequate treatment of non-determinism. We present an semantics extension of the QuantUM approach so that non-determinism is supported with the aid of Markov Decision Processes. We show that the formal semantic interpretation of the UML / SysML models coincides with the code generation semantics for a widely used UML / SysML CASE tool. We evaluate the proposed approach by applying it to two industrial strength case studies, an Airport Surveillance Radar and an Airbag Control Unit.
    Download: [PDF]


  • Florian Leitner-Fischer and Stefan Leue: On the Synergy of Probabilistic Causality Computation and Causality Checking, Technical Report soft-13-01, Chair for Software Engineering, University of Konstanz, 2013.
    Abstract: X
    In recent work on the safety analysis of systems we have shown how causal relationships amongst events can be algorithmically inferred from probabilistic counterexamples and subsequently be mapped to fault trees. The resulting fault trees were significantly smaller and hence easier to understand than the corresponding probabilistic counterexample, but still contain all information needed to discern the causes for the occurrence of a hazard. More recently we have developed an approach called Causality Checking which is integrated into the state-space exploration algorithms used for qualitative model checking and which is capable of computing causality relationships on-the-fly. The causality checking approach outperforms the probabilistic causality computation in terms of run-time and memory consumption, but can not provide a probabilistic measure. In this paper we combine the strengths of both approaches and propose an approach where the causal events are computed using causality checking and the probability computation can be limited to the causal events. We demonstrate the increase in performance of our approach using several case studies.
    Download: [PDF]


  • F. Leitner-Fischer and S.Leue : Causality Checking for Complex System Models, In Proceedings of 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI2013),pp. 248-267, Lecture Notes in Computer Science, Volume 7737. Springer Verlag., 2013.
    Abstract: X
    We present an approach for the algorithmic computation of causalities in system models that we refer to as causality checking. We base our notion of causality on counterfactual reasoning, in particular using the structural equation model approach by Halpern and Pearl that we recently have extended to reason about computational models. In this paper we present a search-based on-the-fly approach that nicely integrates into finite state verification techniques, such as explicit-state model checking. We demonstrate the applicability of our approach using an industrial case study.
    Download: [PDF]


  • 2012

  • A. Bey, S. Leue, C. Wienbruch : A Neuronal Network Model for Simulating the Effects of Repetitive Transcranial Magnetic Stimulation on Local Field Potential Power Spectra, In PLOS ONE, 7(11): e49097, 2012.
    Abstract: X
    Repetitive transcranial magnetic stimulation (rTMS) holds promise as a non-invasive therapy for the treatment of neurological disorders such as depression, schizophrenia, tinnitus, and epilepsy. Complex interdependencies between stimulus duration, frequency and intensity obscure the exact effects of rTMS stimulation on neural activity in the cortex, making evaluation of and comparison between rTMS studies difficult. To explain the influence of rTMS on neural activity (e.g. in the motor cortex), we use a neuronal network model. The results demonstrate that the model adequately explains experimentally observed short term effects of rTMS on the band power in common frequency bands used in electroencephalography (EEG). We show that the equivalent local field potential (eLFP) band power depends on stimulation intensity rather than on stimulation frequency. Additionally, our model resolves contradictions in experiments.
    Download: [PDF]


  • Adrian Beer: Quantitative Analysis of Concurrent System Architectures, Master Thesis, University of Konstanz, 2012.
    Abstract: X
    Safety-critical software and systems development is subject to special dependability requirements. Early analysis of dependability during design and development phase is often a statutory condition for the approval of technical systems. In order to support the developers in verifying and analysing these systems the QuantUM tool was recently introduced. The UML model of the system can be annotated using the presented QuantUM-profile. Afterwards, QuantUM translates the annotated models into the input language of the probabilistic model checker PRISM, which is used as an analysis back-end. This thesis proposes an extension to the QuantUM method so that non-determinism is supported. Non-determinism is an essential paradigm when analysing concurrent system architectures. We introduce new translation rules into the QuantUM profile which are then used to transform UML or SysML models into locally uniform Continuous-Time Markov Decision Processes. Since there are no efficient model checking algorithms for CTMDPs, a discretization technique is applied to convert the CTMDP into discrete-time MDPs. The new approach is applied to two case studies, an Airport Surveillance Radar and an Airbag Control Unit.
    Download: [PDF]


  • Stefan Leue and Mitra Tabaei Befrouei: Counterexample Explanation by Anomaly Detection, Pages 24-42, Proceedings of 19th International SPIN Workshop on Model Checking of Software (SPIN '12), Lecture Notes in Computer Science, Volume 7385. Springer Verlag., 2012.
    Abstract: X
    Since counterexamples generated by model checking tools are only symptoms of faults in the model, a significant amount of manual work is required in order to locate the fault that is the root cause for the presence of counterexamples in the model. In this paper, we propose an automated method for explaining counterexamples that are symptoms of the occurrence of deadlocks in concurrent systems. Our method is based on an analysis of a set of counterexamples that can be generated by a model checking tool such as SPIN. By comparing the set of counterexamples with the set of correct traces that never deadlock, a number of sequences of actions are extracted that aid the model designer in locating the cause of the occurrence of a deadlock. We first argue that the obvious approach to extract such sequences which is by sequential pattern mining and by contrasting patterns that are typical for the deadlocking counterexample traces but not typical for non-deadlocking traces, fails due to the inherent complexity of the problem. We then propose to extract substrings of specific length that only occur in the set of counterexamples for explaining the occurrence of deadlocks. We use a number of case studies to show the effectiveness of our approach and to compare it with an alternative approach to the counterexample explanation problem.
    Download: [PDF]


  • Florian Leitner-Fischer and Stefan Leue: Causality Checking for Complex System Models, Technical Report soft-12-02, Chair for Software Engineering, University of Konstanz. 2012.
    Abstract: X
    With the increasing growth of the size and complexity of modern safety-critical systems, the demand for model based engineering methods that both help in architecting such systems and to asses their safety and correctness becomes increasingly obvious. Causality checking is an automated method for formal causality analysis of system models and system execution traces. In this paper we report on work in progress towards an on-the-fly approach for causality checking of system models. We also sketch how this approach can be applied in model-based system analysis when assessing the system's functional correctness.
    Download: [PDF]


  • Adrian Beer, Uwe Kühne, Florian Leitner-Fischer, Stefan Leue and Rüdiger Prem: Analysis of an Airport Surveillance Radar using the QuantUM approach, Technical Report soft-12-01, Chair for Software Engineering, University of Konstanz. 2012.
    Abstract: X
    We report on the modeling and formal analysis of reliability requirements in the context of an Airport Surveillance Radar system using SysML and probabilistic model checking. The system is modeled using the QuantUM modeling tool which uses the PRISM model checker as an analysis back-end. We illustrate how a complex system architecture can be modeled, what challenges have to be addressed when performing the automated property verification, and to what extent the presented automated analysis method can support the system engineering. We expect that the use of these methods will also have a strong impact on the certification process in future.
    Download: [PDF]


  • Florian Leitner-Fischer and Stefan Leue: Towards Causality Checking for Complex System Models, In Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2012). Dagstuhl, Germany. 2012.
    Abstract: X
    With the increasing growth of the size and complexity of modern safety-critical systems, the demand for model based engineering methods that both help in architecting such systems and to asses their safety and correctness becomes increasingly obvious. Causality checking is an automated method for formal causality analysis of system models and system execution traces. In this paper we report on work in progress towards an on-the-fly approach for causality checking of system models. We also sketch how this approach can be applied in model-based system analysis when assessing the system's functional correctness.
    Download: [PDF]
  • 2011

  • Husain Aljazzar and Stefan Leue: K*: A Heuristic Search Algorithm for Finding the k Shortest Paths, Artificial Intelligence, Volume 175, Number 18, December 2011 2011.
    Abstract: X
    We present a directed search algorithm, called K$^*$, for finding the $k$ shortest paths between a designated pair of vertices in a given directed weighted graph. K$^*$ has two advantages compared to current k-shortest-paths algorithms. First, K$^*$ operates 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$^*$ can be guided using heuristic functions. %This leads to significant improvements in the %memory and runtime demands for many practical problem instances. We prove the correctness of K$^*$ and determine its asymptotic worst-case complexity when using a consistent heuristics to be the same as the state of the art, $\bigo(m + n \log n + k)$, with respect to both runtime and space, where $n$ is the number of vertices and $m$ is the number of edges of the graph. We present an experimental evaluation of K$^*$ by applying it to route planning problems as well as counterexample generation for stochastic model checking. The experimental results illustrate that due to the use of heuristic, on-the-fly search K$^*$ can use less time and memory compared to the most efficient k-shortest-paths algorithms known so far.
    Download: [PDF]


  • Matthias Kuntz, Florian Leitner-Fischer and Stefan Leue: From Probabilistic Counterexamples via Causality to Fault Trees, In Proceedings of 30th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2011), 2011.
    Abstract: X
    Probabilistic Model Checking is an established technique used in the dependability analysis of safety-critical systems. In recent years, several approaches to generate probabilistic counterexamples have been proposed. The interpretation of stochastic counterexamples, however, continues to be problematic since they have to be represented as sets of paths, and the number of paths in this set may be very large. Fault trees (FTs) are a well-established industrial technique to represent causalities for possible system hazards resulting from system or system component failures. In this paper we suggest a method to automatically derive FTs from counterexamples, including a mapping of the probability information onto the FT. We extend the structural equation approach by Pearl and Halpern, which is based on Lewis counterfactuals, so that it serves as a justification for the causality that our proposed FT derivation rules imply. The synthesized FTs provide the user with a concise and compact representation of the causes of potential system failures, together with their respective probabilities. We demonstrate the usefulness of our approach by applying it to a selection of industrial size case studies.
    Download: [PDF]


  • Husain Aljazzar, Florian Leitner-Fischer, Stefan Leue and Dimitar Simeonov: DiPro - A Tool for Probabilistic Counterexample Generation, In Proceedings of 18th International SPIN Workshop on Model Checking of Software (SPIN 2011), 2011.
    Abstract: X
    The computation of counterexamples for probabilistic model checking has been an area of active research over the past years. In spite of the achieved theoretical results in this field, there is no freely available tool that allows for the computation and representation of probabilistic counterexamples. We present an open source tool called DiPro that can be used with the PRISM and MRMC probabilistic model checkers. It allows for the computation of probabilistic counterexamples for discrete time Markov chains (DTMCs), continuous time Markov chains (CTMCs) and Markov decision processes (MDPs). The computed counterexamples can be rendered graphically.
    Download: [PDF]


  • Dominic Lehle: Quantitative Safety Analysis of SysML Models, Bachelor Thesis, University of Konstanz 2011.
    Abstract: X
    Throughout the implementation of safety-critical systems the decision which requirements should be prioritized have to be balanced. It has been often ignored that many failures of a system could have been addressed in early design processes. Despite the lack of well-engineered methods for safety analysis, the costs and complexity often even keep industry giants away from the safety analysis in early stages of the development. Another criteria is that immersed knowledge is required and not often found in industrial methods. In QuantUM, a successful approach of Florian Leitner-Fischer to bridge this gap and improve the integration of quantitative safety analysis methods into the development process, all inputs needed for this type of analysis can be specified at the level of an UML model. However the gap still exists for models which are not principally software-systems. The SysML is a language based on UML and is an established standard in modeling complex and embedded systems in the industry today. Due to the fact that UML includes, in the manner of speaking, the basic principles for SysML, it is convenient to apply and adjust an existent approach in order to bridge the gap in systems engineering. As a result we propose a profile for SysML to enable the specification of all inputs needed for quantitative safety analysis in the early development process, and extend the functionality of the existent software on the level of SysML.
    Download: [PDF]


  • Alina Bey and Stefan Leue: Modeling and Analyzing Spike Timing Dependent Plasticity with Linear Hybrid Automata, Technical Report soft-11-03, Chair for Software Engineering, University of Konstanz. 2011.
    Abstract: X
    We propose a model for synaptic plasticity according to the Spike Timing Dependent Plasticity (STDP) theory using Linear Hybrid Au- tomata (LHA). We first present a compositional LHA model in which each component corresponds to some process in STDP. We then ab- stract this model into a monolithic LHA model in order to enable formal analysis using hybrid model checking. We discuss how the avail- ability of an LHA model as well as its formal analysis using the tool PHAVer can support a better understanding of the dynamics of STDP.
    Download: [PDF]


  • Matthias Kuntz, Florian Leitner-Fischer and Stefan Leue: From Probabilistic Counterexamples via Causality to Fault Trees, Technical Report soft-11-02, Chair for Software Engineering, University of Konstanz. 2011.
    Abstract: X
    Probabilistic Model Checking is an established technique used in the dependability analysis of safety-critical systems. In recent years, several approaches to generate probabilistic counterexamples have been proposed. The interpretation of stochastic counterexamples, however, continues to be problematic since they have to be represented as sets of paths, and the number of paths in this set may be very large. Fault trees (FTs) are a well-established industrial technique to represent causalities for possible system hazards resulting from system or system component failures. In this paper we suggest a method to automatically derive FTs from counterexamples, including a mapping of the probability information onto the FT. We extend the structural equation approach by Pearl and Halpern, which is based on Lewis counterfactuals, so that it serves as a justification for the causality that our proposed FT derivation rules imply. The synthesized FTs provide the user with a concise and compact representation of the causes of potential system failures, together with their respective probabilities. We demonstrate the usefulness of our approach by applying it to a selection of industrial size case studies.
    Download: [PDF]


  • Florian Leitner-Fischer, Stefan Leue: The QuantUM Approach in the Context of the ISO Standard 26262 for Automotive Systems (Extended Abstract), Technical Report soft-11-01, Chair for Software Engineering, University of Konstanz. 2011.
    Abstract: X
    The forthcoming standard ISO 26262 defines processes and techniques in support of a safe design and implementation of automotive systems. We comment on the recommendations that this standard provides with respect to the use of semi-formal and formal methods, including formal verification, during various stages of the proposed safety process. We illustrate how the QuantUM method and tool that we have developed in order to open UML-type system architecture models to formal analysis using stochastic model checking can be applied in support of the safety requirements imposed by the standard.
    Download: [PDF]


  • Matthias Kuntz, Florian Leitner-Fischer, Stefan Leue and Bernd Reh: Challenges in the Modelling and Quantitative Analysis of Safety-Critical Automotive Systems, Presentation at ROCKS workshop (ROCKS 2011). Saarbrücken, Germany. 2011.
    Abstract: X
    In modern cars safety-critical and safety-relevant embedded hard- and software systems are ubiquitous. These systems include systems for active and passive safety such as driving dynamics, braking assistance, and passenger restraint systems such as active control retractors and airbag systems. These systems help to protect car occupants and other road users from potentially fatal injuries. But, the affectees have to rely on the correct functioning of the safety systems. To assure this, a systematic system development begining at the architectural level down to hard- and software implementation is required by the upcoming international norm for functional safety of road vehicles, ISO26262. A norm-compliant development cycle has to prove that the system under consideration satisfies both qualitative and quantitative target measures. Depending on the safety-criticality, the automotive safety integrity level (ASIL) ISO26262 puts tight limits on failure rates for automotive systems. In this work, we will show by means of two different approaches how probabilistic modelling and analysis for the system and hardware level can help to systematically develop automotive safety-critical systems in a way that helps to safe both development time and costs. We will present the quantitative, i.e., probabilistic extension of UML, QuantUM, that can be used to assess the dependability of an automotive system. Secondly, we present a method to use dynamic fault trees to represent probabilistic counter examples to give the system developer a concise overview on desing flaws in case the required ASIL cannot be reached. We will demonstrate the feasibility of the presented approaches by means of an airbag case study, that is derived from a real-world TRW application project.
    Download: [PDF]


  • Florian Leitner-Fischer and Stefan Leue: QuantUM: Quantitative Safety Analysis of UML Models, In Proceedings of Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011). Saarbrücken, Germany. 2011.
    Abstract: X
    When developing a safety-critical system it is essential to obtain an assessment of different design alternatives. In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of available formal quantitative analysis methods it is still difficult for software and system architects to integrate these techniques into their every day work. This is mainly due to the lack of methods that can be directly applied to architecture level models, for instance given as UML diagrams. Also, it is necessary that the description methods used do not require a profound knowledge of formal methods. Our approach bridges this gap and improves the integration of quantitative safety analysis methods into the development process. All inputs of the analysis are specified at the level of a UML model. This model is then automatically translated into the analysis model, and the results of the analysis are consequently represented on the level of the UML model. Thus the analysis model and the formal methods used during the analysis are hidden from the user. We illustrate the usefulness of our approach using an industrial strength case study.
    Download: [PDF]


  • Florian Leitner-Fischer and Stefan Leue: Quantitative Analysis of UML Models, In Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2011). Dagstuhl, Germany. 2011.
    Abstract: X
    When developing a safety-critical system it is essential to obtain an assessment of different design alternatives. In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of available formal quantitative analysis methods it is still difficult for software and system architects to integrate these techniques into their every day work. This is mainly due to the lack of methods that can be directly applied to architecture level models, for instance given as UML diagrams. Our approach bridges this gap and improves the integration of quantitative safety analysis methods into the development process. We propose a UML profile that allows for the specification of all inputs needed for the analysis at the level of a UML model. The QuantUM tool which we have developed, automatically translates an UML model into an analysis model. Furthermore, the results gained from the analysis are lifted to the level of the UML specification or other high-level formalism to further facilitate the process. Thus the analysis model and the formal methods used during the analysis are hidden from the user.
    Download: [PDF]


  • Stefan Leue and Wei Wei: Integer Linear Programming Based Property Checking for Asynchronous Reactive Systems, IEEE Transactions on Software Engineering, vol. 99, 2011.
    Abstract: X
    Asynchronous reactive systems form the basis of a wide range of software systems, for instance in the telecommunications domain. It is highly desirable to rigorously show that these systems are correctly designed. However, traditional formal approaches to the verification of these systems are often difficult because asynchronous reactive systems usually possess extremely large or even infinite state spaces. We propose an Integer Linear Program (ILP) solving based property checking framework that concentrates on the local analysis of the cyclic behavior of each individual component of a system. We apply our framework to the checking of the buffer boundedness and livelock freedom properties, both of which are undecidable for asynchronous reactive systems with an infinite state space. We illustrate the application of the proposed checking methods to Promela, the input language of the SPIN model checker. While the precision of our framework remains an issue, we propose a counterexample guided abstraction refinement procedure based on the discovery of dependencies among control flow cycles. We have implemented prototype tools with which we obtained promising experimental results on real life system models.
    Download: [PDF]
  • 2010

  • Florian Leitner-Fischer: Quantitative Safety Analysis of UML Models, Master Thesis, University of Konstanz, 2010.
    Abstract: X
    When developing a safety-critical system it is essential to obtain an assessment of different design alternatives. In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of available formal quantitative analysis methods it is still difficult for software and system architects to integrate these techniques into their every day work. This is mainly due to the lack of methods that can be directly applied to architecture level models, for instance given as UML diagrams. Another obstacle is, that the methods often require a profound knowledge of formal methods, which can rarely be found in industrial practice. Our approach bridges this gap and improves the integration of quantitative safety analysis methods into the development process. We propose a UML profile that allows for the specification of all inputs needed for the analysis at the level of a UML model. The QuantUM tool which we have developed, automatically translates an UML model into an analysis model. Furthermore, the results gained from the analysis are lifted to the level of the UML specification or other high-level formalism to further facilitate the process. Thus the analysis model and the formal methods used during the analysis are hidden from the user.
    Download: [PDF]


  • Boudewijn R. Haverkort, Matthias Kuntz, Florian Leitner-Fischer, Anne Remke and Stephan Roolvink: Probabilistic verification of Architectural software models using SoftArc and Prism, In: Proceedings of the ESREL 2010 Annual Conference, 5-9 Sept 2010, Greece, Rhodos. pp. 852-860. Taylor & Francis. ISBN 978-0-415-60427-7, 2010.
    Abstract: X
    In this paper we will describe the SoftArc approach. With the SoftArc approach it is possible to model and analyse safety-critical embedded and distributed systems that consist of both hard- and software. We are going to present the SoftArc modelling language, its syntax and semantics. The semantics of the SoftArc modelling language is defined in terms of stochastic reactive modules. We will show how important measures of interest for probabilistic dependability analysis like availability, unavailability, and survivability, i.e., the possibility of a system to recover into an operational mode in the presence of catastrophic events can be formulated and automatically analysed using the SoftArc approach. We will briefly explain how probabilistic FMEA can be done using SoftArc. We will demonstrate the feasibility of our approach by means of three case studies, that involve hard- and software elements. First, we are presenting two industrial case studies from the automotive industry. We will analyse the non volatile random access manager (NVRAM) from the AUTOSAR open system architecture, second we will do a probabilistic FMEA of an airbag control unit. Finally, we are going to present the survivability analysis of a simplified version of the Google file system.
    Download: [PDF]


  • B.R. Haverkort, M. Kuntz, A. Remke, S. Roolvink: Formal Performability Evaluation of Architectural Models of Critical Infrastructures., In: Proceedings of the ESREL 2010 Annual Conference, 5-9 Sept 2010, Greece, Rhodos. pp. 27-34. Taylor & Francis Group. ISBN 978-0-415-60427-7, 2010.
    Abstract: X
    In this paper, we introduce MIOA, a stochastic process algebra-like specification language with finite-domain datatypes, as well as the logic intSPDL, and its model checking algorithms. MIOA which stands for Markovian input/output automata language is an extension of Lynch’s input/output automata with Markovian timed transitions. MIOA can serve both as a fully fledged “stand-alone” specification language and as the semantic model for the architectural dependability description language Arcade. The logic intSPDL is an extension of the stochastic logic SPDL, designed to deal with the specialties of MIOA. In the context of Arcade, intSPDL can be seen as the semantic model of abstract and complex dependability measures that can be defined in the Arcade framework. We define syntax and semantics of both MIOA and intSPDL, and present application examples of MIOA and intSPDL in the realm of dependability modelling with Arcade.
    Download: [PDF]


  • B.R. Haverkort, M. Kuntz, A. Remke, S. Roolvink, M.I.A. Stoelinga: Evaluating Repair Strategies for a Water-Treatment Facility using Arcade, In: 2010 IEEE/IFIP International Conference on Dependable Systems & Networks (DSN), 28 June - 1 July 2010, Chicago, IL, USA. pp. 419-424. IEEE Computer Society Press. ISBN 978-1-4244-7499-8, 2010.
    Abstract: X
    The performance and dependability of critical infrastructures, such as water-treatment facilities is essential. In this paper we use various performance and dependability measures to analyze a simplified model of a water treatment facility. Building on the existing architectural framework Arcade a model is derived in XML format and then automatically mapped to the model checker PRISM. Using the stochastic model checking capabilities that PRISM offers, we compare different repair strategies, with respect to their costs, system reliability, availability and survivability. For this case study we conclude that using non-preemtive priority scheduling with additional repair crews is the best choice with respect to performance, dependability and costs
    Download: [PDF]


  • Matthias Kuntz, Stefan Leue and Christoph Scheben: Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs, Third International Workshop on Invariant Generation (WING 2010), 2010.
    Abstract: X
    Currently, no approaches are known that allow for non-termination proofs of concurrent programs which account for asynchronous communication via FIFO message queues. Those programs may be written in high-level languages such as Java or Promela. We present a first approach to prove non- termination for such programs. In addition to integers, the programs that we consider may contain queues as data structures. We present a representation of queues and the operations on them in the domain of integers, and generate invariants that help us prove non-termination of selected control flow loops using a theorem proving approach. We illustrate this approach by applying a prototype tool implementation to a number of case studies.
    Download: [PDF]


  • Husain Aljazzar and Stefan Leue: K*: Heuristics-Guided, On-the-Fly k Shortest Paths Search, Accepted for publication at Sixth Workshop on Model Checking and Artificial Intelligence (MoChArt 2010), 2010.
    Abstract: X
    We present a search algorithm, called K*, for finding the k shortest paths (KSP) between a designated pair of vertices in a given directed weighted graph. As a directed algorithm, K* has two advantages compared to current KSP algorithms. 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* can be guided using heuristic functions. We prove the correctness of K* and determine its asymptotic worst-case complexity as O(m + n log n + k) with respect to both runtime and space, where n is the number of vertices and m is the number of edges of the graph. We present an experimental evaluation of K* by applying it to route planning problems. The experimental results illustrate the favorable performance of K* compared to the most efficient k-shortest-paths algorithms known so far. In other work it has been shown that K* can be used to efficiently compute counterexamples for stochastic model checking.
    Download: [PDF]


  • Husain Aljazzar and Matthias Kuntz and Florian Leitner-Fischer and Stefan Leue: Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative Evaluation, In: Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems, 2010.
    Abstract: X
    The generation of counterexamples for probabilistic model checking has been an area of active research over the past five years. Tangible outcome of this research are novel directed and heuristic algorithms for efficient generation of probabilistic counterexamples, such as $K^{*}$ and XBF. In this paper we present an empirical evaluation of the efficiency of these algorithms and the well-known Eppstein's algorithm. We will also evaluate the effect of optimizations applied to Eppstein, $K^{*}$ and XBF. Additionally, we will show, how information produced during model checking can be used to guide the search for counterexamples. This is a first step towards automatically generating heuristic functions. The experimental evaluation of the various algorithms is done by applying them to one case study, known from the literature on probabilistic model checking and one case study taken from the automotive industry.
    Download: [PDF]


  • 2009

  • Husain Aljazzar: Directed Diagnostics of System Dependability Models , Doctoral Dissertation, University of Konstanz, 2009.
    Abstract: X
    Model checking, as a formal verification technique, aims primarily at proving the correctness of systems. Nevertheless, model checking has also been extensively used as a debugging technique to aid developers in locating and fixing errors when the model violates a desired property. Thus, the ability to provide diagnostic information, that facilitates debugging, dictates the usability of model checking techniques in practice. Counterexamples are the prime example of such diagnostic information. A counterexample is in general a piece of information which attests the property violation and which can be used for explaining the causal factors of the property violation. Stochastic model checking extends conventional model checking with the verification of quantitative performance and dependability requirements. The core of stochastic model checkers is a set of efficient numerical algorithms which compute the probabilities that determine the satisfaction or violation of a given property. Due to the numerical nature of these algorithms, stochastic model checkers do not provide counterexamples. Within our research in this field we succeeded in extending stochastic model checking to include the possibility of counterexample generation. We introduced the notion of counterexamples into stochastic model checking and devised the first methods for the generation and analysis of counterexamples. We begin this dissertation with an introduction into stochastic model checking followed by a study of counterexamples in stochastic model checking where we give a formal definition for counterexamples for common stochastic models. We also discuss the characteristics of informative counterexamples in this context and present a variety of novel methods for the generation of informative counterexamples. Our methods are based on heuristics-guided search algorithms, also called directed search algorithms. We investigate these methods in different settings and examine their advantages and disadvantages. We also investigate their applicability to models with real-life complexity. We present extensive experiments using significant case studies. These experiments demonstrate the efficiency and scalability of our methods. They also show that the counterexamples produced by our methods are informative and useful for debugging. Counterexamples in stochastic model checking, as we will show in this dissertation, are very complex. Thus, analysing them for the purpose of debugging is a very challenging task for human users. We propose the first method which aids engineers in analysing counterexample in stochastic model checking. Our method employs interactive visualisation techniques which aim at determining the causal factors of property violations. A significant contribution of our research on counterexample generation is the development of a novel directed search algorithm K* for solving the k-shortest-paths problem. This is the problem of finding k shortest paths form a start to a target node in a weighted directed graph for an arbitrary natural number k. The k-shortest-paths problem is a general problem with a wide range of applications. K* scales to very large graphs compared to classical k-shortest-paths algorithms. We demonstrate the advantage of K* by applying it to route planning in the US road map.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • Bahareh Badban, Stefan Leue, Jan-Georg Smaus: Automated Predicate Abstraction for Real-Time Models, INFINITY 2009, 11th International Workshop on Verification of Infinite-State Systems, 2009.
    Abstract: X
    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.
    Download: [PDF]


  • 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: X
    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.
    Download: [PDF]


  • Bahareh Badban: A Term Rewriting Technique for Decision Graphs, in the International Workshop on Computing with Terms and Graphs (TERMGRAPH), 2009.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • Christian Dax, Felix Klaedtke and Stefan Leue: Specification Languages for Stutter-Invariant Regular Properties, In Proceedings of Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Lecture Notes in Computer Science, Springer Verlag, 2009.
    Abstract: X
    We present speci cation languages that naturally capture exactly the regular and w-regular properties that are stutter invariant. Our speci cation languages are variants of the classical regular expres- sions and of the core of PSL, a temporal logic, which is widely used in industry and which extends the classical linear-time temporal logic LTL by semi-extended regular expressions.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 2008

  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • Bahareh Badban: Culling predicates for the Verification of Real-Time Models, Technical Report soft-08-06, Chair for Software Engineering, University of Konstanz, 2008.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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).
    Download: [PDF]


  • 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: X
    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.
    Abstract: X
    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.
    Download: [PDF]


  • Wei Wei: Incomplete Property Checking for Asynchronous Reactive Systems, Doctoral Dissertation, University of Konstanz, 2008.
    Abstract: X
    Not available.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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: X
    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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 2007

  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 2006

  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 2005

  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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: X
    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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 2004

  • 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.
    Abstract: X
    Not available.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 2003

  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 2002

  • 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: X
    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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 2001

  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 2000

  • 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.
    Abstract: X
    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.
    Download: [PDF]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 1999

  • 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: X
    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: X
    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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 1998

  • 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: X
    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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 1997

  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • Stefan Fischer and Stefan Leue: Formal Methods for Broadband and Multimedia Systems , Computer Networks and ISDN Systems, 1997.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 1996

  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 1995

  • 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: X
    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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • Peter B. Ladkin and Stefan Leue: Comments on a Proposed Semantics for Basic Message Sequence Charts , The Computer Journal 37 (9), 1995.
    Abstract: X
    Comments on a Proposed Semantics for Basic Message Sequence Charts, The Computer Journal, 37(9), January 1995.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • Peter B. Ladkin and Stefan Leue: Interpreting Message Flow Graphs , Pages 473 - 509, Formal Aspects of Computing 7(5), 1995.
    Abstract: X
    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.
    Download: [PDF]


  • 1994

  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    Not available.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    Not available.
    Download: [PDF] [PS]


  • 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.
    Abstract: X
    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.
    Download: [PDF] [PS]


  • Stefan Leue: Methods and Semantics for Telecommunications Systems Engineering, Doctoral Dissertation, University of Berne, 1994.
    Abstract: X
    Not available.
    Download: [PDF] [PS]


  • 1993

  • 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: X
    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: X
    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.
    Abstract: X
    Not available.
    Download: [PDF] [PS]


  • 1992

  • Peter B. Ladkin and Stefan Leue: Interpreting Message Sequence Charts, Research Report RJ 8965, IBM Almaden Research Center, 1992.
    Abstract: X
    Not available.