21-07-2014, 01:59 PM
Model Checking for Concurrent Software Architectures
Model Checking.pdf (Size: 1.11 MB / Downloads: 36)
Abstract
The design of concurrent and distributed systems is generally complex, with a high possibility
that subtle errors will cause erroneous behaviour. Behaviour analysis is a powerful technique that
can help to discover behavioural anomalies at design time. The main goal of this thesis is to
develop practical and effective techniques for analysing the behaviour of concurrent and
distributed systems. To be readily usable by software developers, we emphasise that analysis
should go hand in hand with system design. Moreover, analysis techniques should be automated,
intuitive, and effective in detecting errors as well as providing guidance for error correction.
The thesis proposes the TRACTA model-checking approach for analysis of concurrent systems. A
system is modelled as a collection of labelled transition systems (LTSs), which are interacting
finite-state machines. The LTS of the system is computed from the LTSs of its subsystems, and
is checked against desired properties. In TRACTA, analysis is directed by software architecture
and, thus, it is tightly integrated with system design. In our architecture description language
Darwin, a system is described as a hierarchy of components. This hierarchy is exploited for
performing analysis in an incremental way, using Compositional Reachability Analysis (CRA).
TRACTA proposes the ALTL logic for specifying desired properties of a system. ALTL is based
on the linear temporal logic LTL, but it is specialised for concurrent systems modelled as LTSs.
To check that a system satisfies its properties, ALTL formulas are translated into Büchi
automata, following the standard automata-theoretic approach to verification. The uniqueness of
TRACTA lies in the fact that it introduces model checking naturally in CRA, as it proposes
mechanisms addressing issues that arise in this context. In addition to providing a generic
framework for property checking in CRA, the thesis identifies some classes of properties that can
be checked more efficiently. More specifically, practical checking mechanisms are provided for
safety properties as well as for a class of liveness properties, which we refer to as progress.
The thesis provides a simple and efficient way of dealing with fairness. In this context, it
introduces an action priority scheme that allows users to impo
Introduction
With the inevitable increase in complexity of both hardware and software systems, the likelihood
of subtle errors is high. Such errors may have catastrophic consequences in terms of money,
time, or even human life. In general, the earlier an error is discovered, the cheaper it is to fix. In
the industry, there is therefore a growing demand for methodologies that can increase confidence
in correct system design and construction. Such methodologies will result in improved quality, as
well as in a reduction to the total development cost of a system. Additionally, purely on the
theoretical side, there is a need to provide a sound mathematical basis for the design of computer
systems, which can offer practising engineers the confidence of combining their experience with
a solid methodological framework.
Towards usable methods and tools
According to [Clarke and Wing 96a], experience has produced a number of criteria that play a
significant role in making methods and tools attractive to practising engineers. It is important for
such criteria to be taken into consideration if usability is the main goal in developing methods
and tools. In this section, we discuss a set of such criteria that we consider realistic, and which
have motivated our approach to formal verification.
1. Early benefits. In order to encourage practising engineers to use them, methods should
require a minimal effort before engineers realise the benefits from their use. Notations should
be clear and intuitive to the average user. Tools should have friendly user-interfaces that
make them easy to use, and their output should be easy to understand.
2. Incremental gain. Developers should obtain increasing benefit as they put more effort into
learning methods and tools in depth. Ideally, tools should support various modes for users
with various abilities. They should be appealing to the beginner, but should also provide
more sophisticated analysis capabilities for experienced and more demanding users.
3. Integrated use. Analysis should not be an isolated phase in the software development
process. Rather, methods and tools for design, analysis and construction should be well
integrated, and support similar approaches to system development
Scope of this work
Concurrent and distributed systems are no longer rare, but are widely used in applications from
television sets to train signalling and workflow systems. The order in which events occur in the
execution of such systems is unpredictable and only restricted by synchronisation of individual
processes. As a result, the design of distributed systems is generally complex, with a high
probability that subtle errors will cause erroneous behaviour. Without the assistance of automated
tools, it is particularly difficult for the developers of such systems to be confident about the
correctness of their designs.
Our main goal is the development of practical and effective techniques with tool support for
analysing the behaviour of concurrent and distributed systems. More specifically, we focus on
model-checking methods and tools that can be easily introduced into the system development
process, and are accessible to and usable by practising engineers.
The work presented in this thesis builds on previous experience with design and analysis of
distributed systems, within our research team. In our environment, the design of such systems is
based on the description of their software architecture in Darwin [Magee, et al. 95]. Darwin
describes a system as a hierarchy of components that implement services, and additionally
specifies component interactions. It has been extensively used for specifying the structure of
distributed systems and subsequently directing their construction. The Software Architect’s
Contributions
We have developed the TRACTA model-checking approach, which places particular emphasis on
better method and tool usability. The following is an overview of the characteristics and
contributions of TRACTA, based on the usability criteria presented in Section 1.2.
Automation – Error detection and correction
As a model-checking approach, TRACTA is fully automated. The LTSA tool (Figure 1.1), which
currently supports TRACTA, has been based on experience gained from the extensive use of a tool
developed as part of this work [Giannakopoulou, et al. 97]. The LTSA has the advantage of being
implemented in Java, and is therefore cross-platform. It also provides an intuitive user-interface
that facilitates the use of our methods.
Our approach contributes a variety of model-checking mechanisms, as described below.
• TRACTA proposes the logic ALTL (Action Linear Temporal Logic) for specifying desired
properties of a system. ALTL is based on the linear temporal logic LTL [Gribomont and
Wolper 89], but it is specialised for reasoning about concurrent systems modelled as LTSs.
• TRACTA adopts the automata-theoretic approach to model checking [Gribomont and
Wolper 89, Vardi and Wolper 86]. It can check properties expressed directly as Büchi
automata, or as ALTL formulas that are translated into Büchi automata for verification. The
uniqueness of TRACTA lies in the fact that it addresses issues related to model checking in the
context of CRA. It provides efficient model-checking mechanisms that introduce model
checking naturally in our framework, where software architecture is used to direct CRA.
• In addition to generic mechanisms for checking properties expressed as Büchi automata,
TRACTA provides practical analysis strategies for certain classes of properties. Specifically, it
proposes mechanisms for checking safety properties, liveness properties expressed as
deterministic Büchi automata, and a class of liveness properties to which we refer as
progress. All these techniques are integrated in a methodology described in this thesis.
• TRACTA proposes a simple and efficient way of dealing with fairness. In this context, it
introduces an action priority scheme
COSPAN
Cospan [Hardin, et al. 96] takes the automata-theoretic approach to verification. It performs this
by checking inclusion of the language of the system in that of its desirable properties. The native
language is S/R (selection/resolution) but interfaces have been written for the commercial
hardware description languages Vérilog [Thomas and Moorby 98] and VHDL [IEEE 87], as well
as the CCITT-standard protocol specification language SDL [CCITT 93]. The semantic model is
founded on ω-automata. In general, a system consists of a collection of such automata. To
facilitate property specification as ω-automata, a library of parameterised automata is provided.
Counterexamples are returned when property violations are detected in a system. COSPAN can
use either symbolic (BDD-based) or explicit state-enumeration algorithms. The latter invoke
Design & Analysis
To increase the usability of analysis techniques, particular emphasis needs to be placed on the
integration of analysis with other activities of software development. Methods that operate in
isolation may discourage potential users who are burdened with establishing a connection, and
achieving consistency, between the activities supported by these methods. Moreover, information
that is relevant to various phases of system development should ideally need to be provided once,
and be available in the appropriate form for all related activities. This requires the integration not
only of software development methods, but also of the tools that support them.
In TRACTA, the basic structure of a system is described in the Darwin architecture description
language. As Darwin advocates a modular and incremental approach to system development, we
follow a similar approach for behavioural modelling and analysis. This chapter proposes a
compositional model for system behaviour. The structural description of the system can thus be
exploited directly for modelling and analysis. Within this framework, compositional reachability
analysis provides a natural and effective way of dealing with state explosion. The proposed
approach is illustrated by a familiar educational example.
Software architecture in Darwin
Software architecture has been identified as a promising approach to bridge the gap between
requirements and implementations in the design of complex systems [Kramer and Magee 97,
Magee, et al. 97]. Software architecture describes the organisation of a system in terms of its
components and their interactions. It emphasises a separation of concerns; descriptions of
component structure and of component functionality are separate but related activities of
software development.
Analysis Strategies: Safety
In Chapter 4, we have presented a generic mechanism for checking properties expressed either as
formulas of ALTL, or as Büchi automata. The mechanism is powerful enough to handle model
checking in the context of CRA. However, the use of Büchi automata in program verification is
by no means an inexpensive approach. First of all, model checking is performed on the product
of the system with the Büchi automaton; the state space of this product may be significantly
larger than that of the original system. Moreover, a single property is checked at a time. When a
property involves internal actions of subsystems it is composed with that subsystem. The
behaviours of intermediate components affected by the introduction of the property must
therefore be re-computed. Additionally, any change that may affect properties that hold on the
system requires checking these properties again, one at a time.
For some classes of properties or under specific assumptions on the behaviour of a system, model
checking is amenable to strategies that do not suffer from the disadvantages of our generic
mechanism. This chapter proposes such strategies that can be applied for checking safety
properties of a system
Alternating-bit protocol revisited
To illustrate our approach to safety-property checking, we use the example of the alternating-bit
protocol (ABP) presented in Chapter 3. As described, the protocol receiver ignores any message
that is tagged with a different value from the one it expects – the transmitter treats
acknowledgements in a similar way. In order to check the correctness of this mechanism for
identifying superfluous retransmissions of messages and acknowledgements, we introduce
property RIGHT_IGNORE that refers to process RECEIVER. T
Verification
The two versions of the protocol described in Section 3.3.1 have been verified using both
TRACTA and traditional CRA. As discussed above, in order to check the safety properties on this
protocol, both TRACTA and traditional CRA introduce some changes in the system. When a
modification is made in some subsystem, CRA-based methods only need to re-compute the
behaviour of the components affected by the change. The only components that are affected by
the change are the ones marked with block arrows in Figure 5.6. Therefore, the sizes of all
remaining components are as reported in Section 3.4.3. In the tables that display the sizes of the
LTSs obtained with TRACTA and CRA, we only display the modified components.
Discussion
The fact that traditional CRA may need to expose actions at the global system has several
disadvantages. Firstly, it requires careful modification of the interfaces of subsystems in order to
make these actions globally observable. This can be performed directly on the FSP expressions
that describe components of the system. Alternatively, one may modify the component interfaces
in the software architecture (only for the behavioural view), and then re-generate FSP
expressions accordingly. However, such changes may need to be applied each time the developer
identifies new properties to be checked on the system. Secondly, the key to reduction with
compositional minimisation is to employ a modular software architecture and hide as many
internal actions as possible in each subsystem. Exposing internal actions at the global level
compromises the effectiveness of such techniques.
Analysis Strategies: Liveness
In Chapter 5, we mentioned that for some classes of properties or under specific assumptions on
the behaviour of a system, model checking is amenable to strategies that do not suffer from the
disadvantages of our generic mechanism. This chapter proposes such strategies for checking
liveness properties of a system. In this context, we also introduce
Fairness considered
Liveness and fairness are two closely related issues in program verification. When checking
liveness in a program and no notion of fairness has been assumed or incorporated in the model,
the results obtained from verification require to be filtered to a large extent. For example, one
cannot expect that processes of a concurrent program will never starve, when the program runs
on a system with a scheduling policy that does not implement any kind of fairness. Liveness
property violations that are caused by such circumstances are not of interest to the developer.
For example, consider the LTS of Figure 6.1 that represents the joint behaviour of a server and
two clients A and B accessing it. At start-up, the server gets initialised, and then enters a state
where it is ready to receive requests from its clients. After receiving a request (a.req or b.req),
the server delays for some arbitrary time while processing it, and then produces a reply to the
client that made the request (a.reply or b.reply, respectively). One expects that in any
execution of this system, each client is able to regularly communicate with the server. This
means that both a.req and b.req occur infinitely often in any system execution, or, more
Adding fairness constraints to process behaviour
A way of dealing with fairness in model checking is to add Büchi acceptance conditions to the
system. For example in [Aggarwal, et al. 90], the components of a system are modelled as Büchi
automata, and only accepting executions of their product automaton are checked for correctness.
[Gribomont and Wolper 89] describe how a Büchi automaton can be used to express a fair
process scheduler. [Clarke, et al. 86] extend their Kripke models with a set of predicates, so that
fair paths are defined as paths in which each predicate holds infinitely often. This is equivalent to
turning the model of the system into a generalised Büchi automaton. In this way, they can
express both weak and unconditional fairness with respect to processes. However, this requires
the user to modify the initial model of the system.
In TRACTA, Büchi processes can be included in the system in order to impose fairness
constraints. For example, consider the simple client-server system CL_SER illustrated in Figure
6.1. The constraint that a.req and b.req must occur infinitely often in any reasonable execution
of CL_SER can be expressed with the Büchi process FAIR_SERVE of Figure 6.2. By Theorem 4.1,
the product of two Büchi processes accepts the intersection of their languages. Therefore, the
accepting executions of CL_SER|FAIR_SERVE correspond to the fair executions of CL_SER over
its alphabet. This is because, in accepting executions of CL_SER|FAIR_SERVE, both a.req and
b.req occur infinitely often, since both @A and @B must be enabled infinitely often
6.6 Discussion
Our approach to fairness and to progress property checking was motivated by a desire to achieve
a balance between expressive power, accessibility and efficiency. Despite their expressive power,
Büchi automata exacerbate state explosion. Moreover, they are not easy to specify without the
use of an automated tool [Holzmann 97]. In general, this approach to verification is appropriate
for experienced users of an analysis tool, that can handle effectively a formalism like LTL or
Büchi automata to specify properties or fairness assumptions of the system. The effort of using
such a mechanism should only be required by the user if no simpler method is available for
performing the specific analysis of interest.
When Büchi automata are used to express fairness constraints, users not familiar with the
formalism are unable to check their model under any fairness conditions. In such cases, most of
the counterexamples returned by the checking procedure correspond to unrealistic executions of
the system analysed. As model checkers return a single counterexample for a property violation,
the user has no way of finding out if the property checked is really violated, unless the
counterexample is realistic. We believe that, rather than checking liveness with no fairness
constraints and obtaining misleading violations, it is preferable from the developer’s point of
view to get only realistic results from the tool, even at the risk of missing problems that may
occur in practice
Implementation & Evaluation
The TRACTA approach has been motivated by the need to introduce analysis as an integrated part
of system development. In an integrated environment, analysis and modelling should go hand in
hand with design so as to permit distributed systems designers to explore and check their designs
incrementally and naturally. As discussed in previous chapters, TRACTA attempts to address this
requirement by performing analysis based on the software architecture of the system
Environment
The Software Architect’s Assistant (SAA) [Ng, et al. 96] plays the main role in the integration of
our methods. The SAA is a visual environment for the design and development of distributed
programs using Darwin architectural descriptions. Facilities provided include the display of
multiple integrated graphical and textual views, a flexible mechanism for recording design
information and the automatic generation of program code and formatted reports from design
diagrams. The architecture of a system is used by the Darwin compiler to generate a system
instance. The hierarchical structure of a system instance can then be utilised for analysis.
The SAA is currently being re-implemented in Java to aid portability and interoperabili
7.2 Tool implementation
In this section, we describe the main analysis functions of the LTSA and TRACTA tools and
concentrate on the algorithms that implement these functions. Our discussion focuses on those
aspects of the tools that are implementation-independent, and can guide in the extension of
existing tools towards supporting the TRACTA approach. Besides the features that implement the
core of the approach, we also discuss the user-interface and additional features that our tools
provide, which significantly contribute to their usability. Note that, as Büchi processes and LTSs
are treated uniformly by our tools, they are both referred to as LTSs in this chapter
Conclusions
The main goal of the work presented in this thesis has been the development of practical and
effective techniques with tool support for analysing the behaviour of concurrent and distributed
systems. More specifically, we have concentrated on providing methods and tools that can be
easily introduced in the system development process and that are accessible to and usable by
practising engineers. Our work has resulted in the TRACTA model-checking approach. TRACTA
builds on previous experience with CRA techniques developed within our research team [Cheung
94c]. However, in TRACTA, CRA is not simply a reduction technique for state explosion. Rather,
its use is motivated by the need to integrate analysis with system design and construction. In our
environment, software architecture provides the primary link between the various phases of
system development. The hierarchical organisation of the components of the system defined in
its software architecture is used to guide CRA in the construction of system behaviour. Within
this framework, TRACTA contributes several model-checking mechanisms for analysis of
concurrent and distributed systems