Catálogo de publicaciones - libros

The movement to integrate mathematically based software development methods is a predictable response to the fact that none of the many methods available seems sufficient to do the whole job (whatever that may be) on its own. This talk argues that integrating separately developed methods is not the most fruitful possible approach. Instead we propose a family of methods, based on a common model, designed to be complementary and mutually supportive. The method family being developed at the Software Quality Research Lab at the University of Limerick is characterised by two major decisions: – Software developers must prepare and maintain a set of documents whose content (not format) is specified by the relational model presented in [3]. – The relations are represented using mathematical expressions in tabular form. [5]. This talk will motivate these decisions, describe the model, illustrate the concept of tabular expressions, and discuss the uses of such documents in software development.

We provide an automatic method for calculating the path condition for programs with real time constraints. This method can be used for the semiautomatic verification of a unit of code in isolation, i.e., without providing the exact values of parameters with which it is called. Our method can also be used for the automatic generation of test cases for unit testing. The current generalization of the calculation of path condition for the timed case turns out to be quite tricky, since not only the selected path contributes to the path condition, but also the timing constraints of alternative choices in the code.

We review and discuss the current approaches to software model checking, including the complementary views of validation versus falsification and those of static versus dynamic analysis. For falsification, also known as bug finding, we advocate the need for blended approaches that combine the strengths of both static and dynamic analysis. We outline possible directions of research in this area.

The specification matching problem in embedded systems is to determine whether an existing component may be adapted suitably to match the requirements of a new specification . Recently, a refinement called forced simulation has been introduced to formally address this problem. It has been established that when a forced similarity relation exists between a component and its specification, an adapter process can be constructed so that the composition of the adapter and the component fulfil the specification. This looks very similar to synthesis methods in supervisory control theory, where a controller is constructed to make a plant satisfy a desired specification. However, due to the need for state-based hiding in specification matching, supervisory control theory is not directly applicable. This paper develops a supervisory control based solution to the specification matching problem by modifying the problem representation. Subsequently, a comparison of the forced simulation and supervisory control based specification matching methods is made.

In the domain of concurrent software verification, there is an evident need for specification formalisms and efficient algorithms to verify branching-time properties that involve both data and communication. We address this problem by defining a new branching-time temporal logic SE-A ${\it \Omega}$ which integrates both state-based and action-based properties. SE-A ${\it \Omega}$ is universal, i.e., preserved by the simulation relation, and thus amenable to counterexample-guided abstraction refinement. We provide a model-checking algorithm for this logic, based upon a compositional abstraction-refinement loop which exploits the natural decomposition of the concurrent system into its components. The abstraction and refinement steps are performed over each component separately, and only the model checking step requires an explicit composition of the abstracted components. For experimental evaluation, we have integrated our algorithm within the ComFort reasoning framework and used it to verify a piece of industrial robot control software.

It is desirable to integrate formal verification techniques applicable to different languages. We present Exp.Open 2.0, a new tool of the Cadp verification toolbox which combines several features. First, Exp.Open 2.0 allows to describe concurrent systems as a composition of finite state machines, using either synchronization vectors, or parallel composition, hiding, renaming, and cut operators from several process algebras ( Ccs , Csp , Lotos , E-Lotos , μ Crl ).Second, together with other tools of Cadp , Exp.Open 2.0 allows state space generation and on-the-fly exploration. Third, Exp.Open 2.0 implements on-the-fly partial order reductions to avoid the generation of irrelevant interleavings of independent transitions.Fourth, Exp.Open 2.0 allows to export models towards other tools using interchange formats such as automata networks and Petri nets.Finally, we show some practical applications and measure the efficiency of Exp.Open 2.0 on several benchmarks.

CSP ∥ B is an approach to combining the process algebra CSP with the formal development method B, enabling the formal description of systems involving both event-oriented and state-oriented aspects of behaviour. The approach provides architectures which enable the application of CSP verification tools and B verification tools to the appropriate parts of the overall description. Previous work has considered how large descriptions can be verified using coarse grained component parts. This paper presents a generalisation of that work so that CSP ∥ B descriptions can be decomposed into finer grained components, chunks , which focus on demonstrating the absence of particular divergent behaviour separately. The theory underpinning chunks is applicable not only to CSP ∥ B specification but to CSP specifications. This makes it an attractive technique to decomposing large systems for analysing with FDR.

Software development methods are software products, in the sense that they should be engineered by following a methodology to meet the behavioural and non-behavioural requirements of the intended users of the method. We argue that agile approaches are the most appropriate means for engineering new methods, and particularly for integrating formal methods. We show how agile principles and practices apply to engineering methods, and demonstrate their application by integrating parts of the Eiffel development method with CSP.

Formal methods have significant benefits for developing safety critical systems, in that they allow for correctness proofs, model checking safety and liveness properties, deadlock checking, etc. However, formal methods do not scale very well and demand specialist skills, when developing real-world systems. For these reasons, development and analysis of large-scale safety critical systems will require effective integration of formal and informal methods. In this paper, we use such an integrative approach to automate Failure Modes and Effects Analysis (FMEA), a widely used system safety analysis technique, using a high-level graphical modelling notation (Behavior Trees) and model checking. We inject component failure modes into the Behavior Trees and translate the resulting Behavior Trees to SAL code. This enables us to model check if the system in the presence of these faults satisfies its safety properties, specified by temporal logic formulas. The benefit of this process is tool support that automates the tedious and error-prone aspects of FMEA.

In this paper, we present the idea of creating an intermediary model which is capable of being derived directly from the high-level, abstract model, but more closely resembles the actual implementation. The focus of our work is on the security properties of protocols. Not only do we show how an intermediary model can be constructed, but also how it can be used to automatically generate test sequences based on the security goals of the protocol being tested. Our aim is to show that by using this approach, we can derive test sequences suitable for a tester to use on a working implementation of the protocol.