Buy issue PDF
- $293.80
IET Software
Volume 4, issue 3, June 2010
Volumes & issues:
Volume 4, issue 3
June 2010
-
- Author(s): D. Giannakopoulou; C.S. Pãsãreanu
- + Show Description
-
Hide details
-
p.
179
–180
(2)
- Author(s): S. Bensalem; M. Bozga; T.-H. Nguyen; J. Sifakis
- + Show Description
-
Hide details
-
p.
181
–193
(13)
The authors present a compositional method for the verification of component-based systems described in a subset of the behaviour-interaction-priority language encompassing multi-party interaction without data transfer. The method is based on the use of two kinds of invariants. Component invariants are over-approximations of components' reachability sets. Interaction invariants are global constraints on the states of components involved in interactions. The method has been implemented in the D-Finder tool and has been applied for checking deadlock-freedom. The experimental results on non-trivial examples show that this method allows either to prove deadlock-freedom or to identify very few deadlock configurations that can be analysed by using state-space exploration. - Author(s): O. Tkachuk; M.B. Dwyer
- + Show Description
-
Hide details
-
p.
194
–209
(16)
Event-driven systems maintain an ongoing dialog with their environment. Examples include: distributed programs, where each process reacts to received messages by performing computation and sending messages to peers; graphical user interfaces (GUI), where the interface software and the underlying application react to user inputs and web-based applications, where presentation, business logic and storage tier functionality react to user inputs and response from other web-based services. Such applications are difficult to test because the set of possible interaction sequences between the system and its environment can be very large and governed by complex constraints. The exhaustive nature of software model checking techniques offers hope for effectively validating such systems, however, they only work for closed systems. Previously, the authors developed the Bandera Environment Generator, which given an open system, called a unit under analysis, closes it with a model of its environment. The authors' previous work on environment generation has focused on developing broadly applicable mechanisms for modelling environment behaviour. The generality of this approach often makes it difficult to produce environment models that enable precise and efficient system analysis. The authors' experience shows that by exploiting information about the application domain, generated environments can be made both more precise and more efficient for model checking. This study presents the concept of domain-specific environment generation, details techniques for customising environment generation for the domain of event-driven software, and assesses those techniques on the domains of GUI and web-based applications. - Author(s): P. Parizek; F. Plasil
- + Show Description
-
Hide details
-
p.
210
–221
(12)
A key problem in compositional model checking of software systems is that typical model checkers accept only closed systems (runnable programs) and therefore a component cannot be model-checked directly. A typical solution is to create an artificial environment for the component such that its composition forms a runnable program that can be model-checked. Although it is possible to create a universal environment that performs all possible sequences and interleavings of calls of the component's methods, for practical purposes it is sufficient to capture in this way just the use of the component in a particular software system – this idea is expressed by the paradigm of assume-guarantee reasoning. The authors present an approach to assume-guarantee-based verification of software systems in the context of the SOFA 2 component framework. They provide an overview of the approach to the construction of an artificial environment for the verification of SOFA 2 components implemented in Java with the Java PathFinder model checker. They also show the benefits of their approach on results of experiments with a non-trivial software system and discuss its advantages over other approaches with similar goals. - Author(s): B. Finkbeiner; H.-J. Peter; S. Schewe
- + Show Description
-
Hide details
-
p.
222
–235
(14)
The authors present an automatic method for the synthesis of certificates for components in embedded real-time systems. A certificate is a small homomorphic abstraction that can transparently replace the component during model checking: if the verification with the certificate succeeds, then the component is guaranteed to be correct; if the verification with the certificate fails, then the component itself must be erroneous. The authors give a direct construction, based on a forward and backward reachability analysis of the timed system, and an iterative refinement process, which produces a series of successively smaller certificates. In their experiments, model checking the certificate is several orders of magnitude faster than model checking the original system.
Editorial: Automated compositional verification
Compositional verification for component-based systems and application
Environment generation for validating event-driven software using model checking
Assume-guarantee verification of software components in SOFA 2 framework
Synthesising certificates in networks of timed automata
