- Viet Yen Nguyen, Benjamin Bittner, Joost-Pieter Katoen and Thomas Noll.
Compositional Analysis Using Component-Oriented Interpolation.
In: Proceedings of the 11th International Symposium on Formal Aspects of Component Software (FACS) pages 68-85, Volume 8997 of LNCS, Springer.
Recipient of the EASST Best Paper Award
[abstract]
We present a novel abstraction technique that exploits the compositionality of a concurrent system consisting of interacting components. It uses, given an invariant and a component of interest, bounded model checking (BMC) to quickly interpolate an abstraction of that component's environment. The abstraction may be refined by increasing the BMC bound. Furthermore, it is only defined over variables shared between the component and its environment, resulting in an aggressive abstraction with several applications. We demonstrate its use in a verification setting, as we report on our open source implementation in the NuSMV model checker which was used to perform a practical assessment with industrially-sized models from satellite case studies of ongoing missions. These models are expressed in a formalized dialect of the component-oriented and industrially standardized Architecture Analysis and Design Language (AADL).
- Dimitri Bohlender, Harold Bruintjes, Sebastian Junges, Jens Katelaan, Viet Yen Nguyen, Thomas Noll.
A Review Of Statistical Model Checking Pitfalls on Real-Time Stochastic Models.
In: Proceedings of the 6th International Symposium of Leveraging Applications of Formal Methods, Verification and Validation (ISOLA) pages 177-192, Volume 8803 of LNCS, Springer.
[abstract]
Statistical model checking (SMC) is a technique inspired by Monte-Carlo simulation for verifying time-bounded temporal logical properties. SMC originally focused on fully stochastic models such as Markov chains, but its scope has recently been extended to cover formalisms that mix functional real-time aspects, concurrency and non-determinism. We show by various examples using the tools UPAAL and MODES that combining the stochastic interpretation of such models with SMC algorithms is extremely subtle. This may yield significant discrepancies in the analysis results. As these subtleties are not so obvious to the end-user, we present five semantic caveats and give a classification scheme for SMC algorithms. We argue that caution is needed and believe that the caveats and classification scheme in this paper serve as a guiding reference for thoroughly understanding them.
- Bernhard Ern, Viet Yen Nguyen, Thomas Noll.
Characterization of Failure Effects on AADL Models.
In: Proceedings of the 32nd International Conference on Computer Safety, Reliability and Security (SAFECOMP) pages 241-252, Volume 8153 of LNCS, Springer, 2013.
[abstract]
Abstract: Prior works on model-based Failure Modes and Effects Analysis (FMEA) automatically generate a FMEA table given the system model, a set of failure modes, and a set of possible effects. The last requirement is critical as bias may occur: since the considered failure effects are restricted to the anticipated ones, unexpected effects - the most interesting ones - are disregarded in the FMEA.
In this paper, we propose and investigate formal concepts that aim to overcome this bias. They support the construction of FMEA tables solely based on the system model and the failure modes, i.e., without requiring the set of effects as input. More concretely, given a system specification in the Architecture Analysis and Design Language (AADL), we show how to derive relations that characterize the effects of failures based on the state transition system of that specification. We also demonstrate the benefits and limitations of these concepts on a satellite case study.
- Marie-Aude Esteve, Joost-Pieter Katoen, Viet Yen Nguyen, Bart Postma, Yuri Yushtein.
Formal Correctness, Safety, Dependability and Performance Analysis of a Satellite.
In: Proceedings of the 34th International Conference on Software Engineering (ICSE) pages 1022-1031, IEEE, 2012.
[abstract]
Abstract: This paper reports on the usage of a broad palette of formal modeling and analysis techniques on a regular industrial-size design of an ultra-modern satellite platform. These efforts were carried out in parallel with the conventional software development of the satellite platform. The model itself is expressed in a formalized dialect of AADL. Its formal nature enables rigorous and automated analysis, for which the recently developed COMPASS toolset was used. The whole effort revealed numerous inconsistencies in the early design documents, and the use of formal analyses provided additional insight on discrete system behavior (comprising nearly 50 million states), on hybrid system behavior involving discrete and continuous variables, and enabled the automated generation of large fault trees (66 nodes) for safety analysis that typically are constructed by hand. The model's size pushed the computational tractability of the algorithms underlying the formal analyses, and revealed bottlenecks for future theoretical research. Additionally, the effort led to newly learned practices from which subsequent formal modeling and analysis efforts shall benefit, especially when they are injected in the conventional software development lifecycle. The case demonstrates the feasibility of fully capturing a system-level design as a single comprehensive formal model and analyze it automatically using a toolset based on (probabilistic) model checkers.
- Yuri Yushtein, Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Xavier Olive, Marco Roveri.
System-Software Co-Engineering: Dependability and Safety Perspective.
In: Proceedings of the 4th IEEE International Conference on Space Mission Challenges in Information Technology (SMC-IT) pages 18-25, IEEE, 2011.
[abstract]
Abstract: The need for an integrated system-software co-engineering framework to support the design of modern space systems is pressing. The current tools and formalisms tend to be tailored to specific analysis techniques and are not amenable for the full spectrum of required system aspects such as safety, dependability and performability. Additionally, they cannot handle the intertwining of hardware and software interaction. As such, the current practices lack integration and coherence. We recently developed a coherent and multidisciplinary approach towards developing space systems at architectural design level, linking all of the aforementioned aspects, and assessed it with several industrial evaluations. This paper reports on the approach, the evaluations and our perspective on current and future developments.
- Maximilian R. Odenbrett, Viet Yen Nguyen, Thomas Noll.
Slicing AADL Specifications for Model Checking.
In: Proceedings of the 2nd NASA Formal Methods Symposium (NFM) pages 217-221, Volume of NASA Conference Proceedings, 2010.
[abstract]
Abstract: To combat the state-space explosion problem in model checking larger systems, abstraction techniques can be employed. Here, methods that operate on the system specification before constructing its state space are preferable to those that try to minimize the resulting transition system as they generally reduce peak memory requirements. We sketch a slicing algorithm for system specifications written in (a variant of) the Architecture Analysis and Design Language (AADL). Given a specification and a property to be verified, it automatically removes those parts of the specification that are irrelevant for model checking the property, thus reducing the size of the corresponding transition system. The applicability and effectiveness of our approach is demonstrated by analyzing the state-space reduction for an example, employing a translator from AADL to Promela, the input language of the SPIN model checker.
- Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Xavier Olive.
Formal Verification and Validation of AADL Models.
In: Proceedings of Embedded Real Time Software and Systems Conference (ERTSS), 2010.
[abstract]
Introduction: Safety-critical systems are increasingly difficult to comprehend due to their rising complexity. Methodologies, tools and modeling formalisms have been developed to overcome this. Component-based design is an important paradigm that is shared by many of them. It helps to master the overall complexity while in addition allowing for reusability. Furthermore, it easily supports the common issues in the engineering disciplines, like hardware/software (i.e., co-engineering), performability, dependability, reliability, availability, maintainability and safety engineering (RAMS). Model artifacts that are typical for a discipline can be encapsulated in the affected components, while staying imperceptible for non-affected components. This leads to different views of the system under development, which subsequently entails the natural distinction in different system abstractions, formalisms and tools. Nonetheless, there is only one system under development. With the current methodologies, there is no single view of this system that links all aspects relevant to all involved engineering disciplines in a coherent manner.
- Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri, Ralf Wimmer.
A Model Checker for AADL.
In: Proceedings of 22nd International Conference on Computer Aided Verification (CAV) pages 562-565, Volume 6174 of LNCS, Springer, 2010.
[abstract]
Abstract: We present a graphical toolset for verifying AADL models, which are gaining widespread acceptance in aerospace, automobile and avionics industries for comprehensively specifying safety-critical systems by capturing functional, probabilistic and hybrid aspects. Analyses are implemented on top of mature model checking tools and range from requirements validation to functional verification, safety assessment via automatic derivation of FMEA tables and dynamic fault trees, to performability evaluation, and diagnosability analysis. The toolset is currently being applied to several case studies by a major industrial developer of aerospace systems.
- Falko Dulat, Joost-Pieter Katoen, Viet Yen Nguyen.
Model Checking Markov Chains using Krylov Subspace Methods: An Experience Report.
In: Proceedings of 7th European Performance Engineering Workshop (EPEW) pages 115-130, Volume 6342 of LNCS, Springer, 2010.
[abstract]
Abstract: The predominant technique for computing the transient distribution of a Continuous Time Markov Chain (CTMC) exploits uniformization, which is known to be stable and efficient for non-stiff to mildly-stiff CTMCs. On stiff CTMCs however, uniformization suffers from severe performance degradation. In this paper, we report on our observations and analysis of an alternative technique using Krylov subspaces. We implemented a Krylov-based extension to MRMC (Markov Reward Model Checker) and conducted extensive experiments on five case studies from different application domains. The results reveal that the Krylov-based technique is an order of magnitude faster on stiff CTMCs.
- Marco Bozzano, Alessandro Cimatti, Marco Roveri, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll.
Codesign of Dependable Systems: A Component-Based Modeling Language.
In: Proceedings 7th ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE) pages 121-130, IEEE, 2009.
[abstract]
Abstract: This paper presents a model-based approach to system-software co-engineering which is focused on aerospace systems but is relevant to a much wider class of dependable systems. We present the main ingredients of the SLIM modeling language and give a precise interpretation of SLIM models by providing a formal semantics using networks of event-data automata. The major distinguishing aspects of this component-based approach are the possibility to describe nominal hardware and software operations, hybrid (and timing) aspects, as well as probabilistic faults and their propagation and recovery. As our approach bears strong resemblance to the standardized AADL (Architecture Analysis and Design Language), a secondary contribution of this paper is a formal semantics of a large fragment of AADL including its Error Model Annex.
- Viet Yen Nguyen, Theo C. Ruys.
Memoised Garbage Collection for Software Model Checking.
In: Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) pages 201-214, Volume 5505 of LNCS, Springer, 2009.
[abstract]
Abstract: Virtual machine based software model checkers like jpf and MoonWalker spend up to half of their verification time on garbage collection. This is no surprise as after nearly each transition the heap has to be cleaned from garbage. To improve this, this paper presents the Memoised Garbage Collection (MGC) algorithm, which exploits the (typical) locality of transitions to incrementally perform garbage collection. MGC tracks the depths of objects efficiently and only purges objects whose depths have become infinite, hence unreachable. MGC was experimentally evaluated via an implementation in our model checker MoonWalker and benchmarks using the parallel Java Grande Forum benchmark suite. By using MGC, a performance increase up to 78% was measured over the traditional Mark&Sweep implementation.
- Niels H.M. Aan de Brugh, Viet Yen Nguyen, Theo C. Ruys.
MoonWalker: Verification of .NET Programs.
In: Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) pages 170-173, Volume 5505 of LNCS, Springer, 2009.
[abstract]
Abstract: MoonWalker is a software model checker for cil bytecode programs, which is able to detect deadlocks and assertion violations in cil assemblies, better known as Microsoft .NET programs. The design of MoonWalker is inspired by the Java PathFinder (jpf), a model checker for Java programs. The performance of MoonWalker is on par with jpf. This paper presents the new version of MoonWalker and discusses its most important features.
- Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri.
The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems.
In: Proceedings of the 28th International Conference on Computer Safety, Reliability and Security (SAFECOMP) pages 173-186, Volume 5775 of LNCS, Springer, 2009.
[abstract]
Abstract: We report on a model-based approach to system-software co-engineering which is tailored to the specific characteristics of critical on-board systems for the aerospace domain. The approach is supported by a System-Level Integrated Modeling (SLIM) Language by which engineers are provided with convenient ways to describe nominal hardware and software operation, (probabilistic) faults and their propagation, error recovery, and degraded modes of operation.
Correctness properties, safety guarantees, and performance and dependability requirements are given using property patterns which act as parameterized “templates” to the engineers and thus offer a comprehensible and easy-to-use framework for requirement specification. Instantiated properties are checked on the SLIM specification using state-of-the-art formal analysis techniques such as bounded SAT-based and symbolic model checking, and probabilistic variants thereof. The precise nature of these techniques together with the formal SLIM semantics yield a trustworthy modeling and analysis framework for system and software engineers supporting, among others, automated derivation of dynamic (i.e., randomly timed) fault trees, FMEA tables, assessment of FDIR, and automated derivation of observability requirements.
- Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri.
Verification and Performance Evaluation of AADL Models (Tool Demonstration).
In: Proceedings of the 7th Joint Meeting of European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE) pages 285-286, ACM, 2009.
[abstract]
Abstract: This paper reports on a model-based approach to system-software co-engineering which is tailored to critical on-board systems for the aerospace domain but is relevant to a much wider class of dependable systems. Our main contribution is a formal semantics for a greater part of standardised AADL, the Architecture Analysis and Design Language, and its Error Model Annex. It covers nominal and degraded hardware/software operations, hybrid (and timing) aspects as well as probabilistic faults, their propagation and recovery. The accompanying software toolset employs SAT-based and symbolic model checking techniques and probabilistic variants thereof. The precise nature of these techniques together with the formal semantics provide a trustworthy modelling and analysis framework to support, among others, assessment of functional correctness, evaluation of performance measures and automated derivation of dynamic fault trees, FMEA tables and observability requirements.
- Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri.
Model-Based Codesign of Critical Embedded Systems.
In: Proceedings of the 2nd International Workshop on Model Based Architecting and Construction of Embedded Systems (ACES-MB) pages 87-91, Volume 507 of CEUR Workshop Proceedings, 2009.
[abstract]
Abstract: We present a comprehensive methodology for the specification and
analysis of critical embedded systems. The methodology is based on an
architectural design language that enables modeling of both software
and hardware components, timed and hybrid behavior, faulty behavior
and degraded modes of operation, error propagation and recovery. The
methodology is supported by an integrated platform, implemented on top
of state-of-the-art tools, that provides verification capabilities
ranging from requirements analysis to functional verification, safety
assessment, performability evaluation, diagnosis and diagnosability.
- Viet Yen Nguyen, Theo C. Ruys.
Incremental Hashing for SPIN.
In: Proceedings of the 15th International SPIN Workshop on Model Checking Software pages 232-249, Volume 5156 of LNCS, Springer, 2008.
[abstract]
Abstract: This paper discusses a generalised incremental hashing scheme for explicit state model checkers. The hashing scheme has been implemented into the model checker Spin. The incremental hashing scheme works for Spin’s exhaustive and both approximate verification modes: bitstate hashing and hash compaction. An implementation is provided for 32-bit and 64-bit architectures.
We performed extensive experiments on the BEEM benchmarks to compare the incremental hash functions against Spin’s traditional hash functions. In almost all cases, incremental hashing is faster than traditional hashing. The amount of performance gain depends on several factors, though.
We conclude that incremental hashing performs best for the (64-bits) Spin’s bitstate hashing mode, on models with large state vectors, and using a verifier, that is optimised by the C compiler.