Catálogo de publicaciones - libros

This paper presents a formal but practical approach for defining and using design patterns. Initially we formalize the concepts commonly used in defining design patterns using Object-Z. We also formalize consistency constraints that must be satisfied when a pattern is deployed in a design model. Then we implement the pattern modeling language and its consistency constraints using an existing modeling framework, EMF, and incorporate the implementation as plug-ins to the Eclipse modeling environment. While the language is defined formally in terms of Object-Z definitions, the language is implemented in a practical environment. Using the plug-ins, users can develop precise pattern descriptions without knowing the underlying formalism, and can use the tool to check the validity of the pattern descriptions and pattern usage in design models. In this work, formalism brings precision to the pattern language definition and its implementation brings practicability to our pattern-based modeling approach.

We consider modelling indispensable for the development of complex systems. Modelling must be carried out in a formal notation to reason and make meaningful conjectures about a model. But formal modelling of complex systems is a difficult task. Even when theorem provers improve further and get more powerful, modelling will remain difficult. The reason for this that modelling is an exploratory activity that requires ingenuity in order to arrive at a meaningful model. We are aware that automated theorem provers can discharge most of the onerous trivial proof obligations that appear when modelling systems. In this article we present a modelling tool that seamlessly integrates modelling and proving similar to what is offered today in modern integrated development environments for programming. The tool is extensible and configurable so that it can be adapted more easily to different application domains and development methods.

Model Based Development (MBD) using Mathworks tools like Simulink, Stateflow etc. is being pursued in Honeywell for the development of safety critical avionics software. Formal verification techniques are well-known to identify design errors of safety critical systems reducing development cost and time. As of now, formal verification of Simulink design models is being carried out manually resulting in excessive time consumption during the design phase. We present a tool that automatically translates certain Simulink models into input language of a suitable model checker. Formal verification of safety critical avionics components becomes faster and less error prone with this tool. Support is also provided for reverse translation of traces violating requirements (as given by the model checker) into Simulink notation for playback.

The verification of information flow properties of security devices is difficult because it involves the analysis of schematic diagrams, artwork, embedded software, etc. In addition, a typical security device has many modes, partial information flow, and needs to be fault tolerant. We propose a new approach to the verification of such devices based upon checking abstract information flow properties expressed as graphs. This approach has been implemented in software, and successfully used to find possible paths of information flow through security devices.

Computer networks have become ubiquitous in our society and thus, the various types of resources hosted by them are becoming increasingly important. In this paper we study the resource availability in networks by defining a dedicated middleware language. This language is a conservative extension of the action system formalism, a general state-based approach to modeling and analyzing distributed systems. Our language formally treats aspects such as resource accessibility, replicated and homonym resources, their mobility, as well as node failure and maintenance in networks. The middleware approach motivates the separation of the views and formalisms used by the various roles such as the network user, the application developer, and the network manager.

We introduce a method to elicit and to structure using Event B, processes interacting with ad hoc dynamic architecture. A Group Communication System is used as the investigation support. The method takes account of the evolving structure of the interacting processes; it guides the user to structure the abstract system that models his/her requirements. The method also integrates property verification using both theorem proving and model checking. A B specification of a GCS is built using the proposed approach and its stated properties are verified using a B theorem prover and a B model checker.

In this paper we discuss some issues in implementing a model checker for the Z specification language. In particular, the language design of Z and its semantics, raises some challenges for efficient model checking, and we discuss some of these issues here. Our approach to model checking Z specifications involves implementing a translation from Z into the SAL input language, upon which the SAL toolset can be applied. In this paper we discuss issues in the implementation of this translation algorithm and illustrate them by looking at how the mathematical toolkit is encoded in SAL and the resultant efficiency of the model checking tools.

In this paper, we advocate the use of formal specification and verification in software development for high-integrity and safety-critical systems, where mechanical proof plays a central role. In particular, we emphasise the crucial importance of applying verification in the development of formal verification tools themselves. We believe this approach is very useful to increase the levels of confidence and integrity of tools that are built to find bugs based on formally specified models. This follows the trend set out by a UK grand challenge in computer research for verified software repository. In this direction, we present our experiences on a case study on the development process of a refinement model checking tool for Circus , a concurrent refinement language that combines Z, CSP, guarded commands, and the refinement calculus, with the Unifying Theories of Programming of Hoare and He as the theoretical background.

Software specifications are of great use for more rigorous software development. They are useful for formal verification and automated testing, and they improve program understanding. In practice, specifications often do not exist and developers write software in an ad-hoc fashion. We describe a new way to automatically infer specifications from code. Our approach infers a likely specification for any method such that the method’s behavior, i.e., its effect on the state and possible result values, is summarized and expressed in terms of some other methods. We use symbolic execution to analyze and relate the behaviors of the considered methods. In our experiences, the resulting likely specifications are compact and human-understandable. They can be examined by the user, used as input to program verification systems, or as input for test generation tools for validation. We implemented the technique for .NET programs in a tool called Axiom Meister. It inferred concise specifications for base classes of the .NET platform and found flaws in the design of a new library.

We introduce a formal, time aware framework for modelling and analysis multiclocked VLSI systems. We define a delay calculus framework for our timed formalism, and, furthermore, constraints with which to confine the correctness of the system under development, not only logically but also with respect to timing characteristics. We give an elaborate definition of the timed formalism, Timed Action Systems, and its delay models. With the timing aware formal development framework it is possible to obtain information of multiclocked VLSI systems already at high abstraction levels as our application, a GALS (globally asynchronous, locally synchronous) system, shows.