I will be speaking at the 3rd International Conference Applying ISO 26262 on Thursday March, 21 2013. The title of my talk is ”Model-based Engineering and ISO26262″ and I will talk about our experiences in using model-based engineering in an ISO 26262 context and lessons learned that we identified. If you are at the conference and are interested in model-based engineering we should talk!
Mar 18
Jan 21
I gave a talk on causality checking for complex system models at the VMCAI 2013 conference in Rome, Italy.
The slides of my talk are available here.
Abstract:
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.
Jul 18
I just discovered a great new (?) feature of Google Scholar called author profiles.
There a two great benefits:
- You can “follow” authors and automatically get an email alert whenever they have published a paper, in my opinion a great way to keep track of what is going on in your research field.
- You can “follow” citations of authors and for instance automatically get an email alert when somebody cites your paper.
A minor but still interesting point is that you can create a public or private author profile where
- all your publications are listed,
- metrics like citation count, h-index, i10-index and so on are computed,
- and you can enter a link to your current website.
Jun 20
After many months of implementation and testing we finally released the DiPro tool for probabilistic counterexample generation tool.
I will give a talk on DiPro’s features on the SPIN 2011 Workshop (July 14-15), co-located with CAV 2011 in Snowbird Utah.
What is DiPro?
Current stochastic model checkers do not make counterexamples for property violations readily available. DiPro is a tool, that applies 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 DiPro very efficient and highly scalable. They can also be guided using heuristics which usually improve the performance of the method.
Counterexamples provided by DiPro 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.
DiPro allows for the computation of counterexamples for the stochastic model checkers PRISM or MRMC.
Nov 19
My master’s thesis is now available online here.
Abstract
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.
Oct 16
Our recently published case study “Safety Analysis of an Airbag System using Probabilistic FMEA and Probabilistic Counter Examples” is the cover story over the newest issue of UNIKON the magazine of the University of Konstanz.
Dec 05
The paper “Simulink Design Verifier vs. SPIN – A Comparative Case Study” which was joint work with Stefan Leue and was presented at FMICS 08 is now available online.The paper is more or less a summary of my bachelor thesis.
Aug 19
My bachelor thesis “Evaluation of the Matlab Simulink Design verifier vs. the model checker SPIN” is now available online at http://www.ub.uni-konstanz.de/kops/volltexte/2008/6125/
Aug 02
I recently finished my bachelor thesis and will present a part of it as a short paper at the 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS) in L’Aquila, Italy.
Simulink Design Verifier vs. SPIN – A Comparative Case Study Florian Leitner and Stefan Leue
Keywords
State Space Exploration, Matlab Simulink, SPIN, Automotive SoftwareAbstract
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 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 Verifier 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 suitability to verify a set of basic system properties, and quantitative in comparing the computational efficiency of both tools.
