Catálogo de publicaciones - libros

The web site for this conference states that: “The challenge now is to achieve general acceptance of formal methods as a part of industrial development of high quality systems, particularly trusted systems.” We are all going to be discussing How to achieve this, but before that we should maybe ask the other questions: What are the real benefits of formal methods and Why should we care about them? When and Where should we expect to use them, and Who should be involved? I will suggest some answers to those questions and then describe some ways that the benefits are being realised in practice, and what I think needs to happen for them to become more widespread.

We provide precise high-level models for eight fundamental service interaction patterns, together with schemes for their composition into complex service-based business process interconnections and interaction flows, supporting software-engineered business process management in multi-party collaborative environments. The mathematical nature of our models provides a basis for a rigorous execution-platform-independent analysis, in particular for benchmarking web services functionality. The models can also serve as accurate standard specifications, subject to further design leading by stepwise refinement to implementations.

Theorem provers, model checkers, static analyzers, test generators...all of these and many other kinds of formal methods tools can contribute to the analysis and development of computer systems and software. It is already quite common to use several kinds of tools in a loose combination: for example, we might use static analysis and then model checking to help find and eliminate design flaws prior to undertaking formal verification with a theorem prover. And some modern tools, such as test generators, are built using model checkers, predicate abstractors, decision procedures and constraint solvers as components in tight combination. But we can foresee a different kind of combination where many tools and methods are used in ad hoc combination within a single analysis. For example, static analysis might yield invariants that enable decision procedures to build a predicate abstraction whose reachable states are calculated as a BDD and then concretized to yield a strong invariant for the original system; the invariant then enables properties of the original system to be verified by highly automated theorem proving. This sort of combination clearly requires an integrating platform – a tool bus – to connect the various tools together; but the capabilities required go beyond those of platforms such as Eclipse. The entities exchanged among clients of the bus – proofs, counterexamples, specifications, theoreems, counterexamples, abstractions – have logical content, and the overall purpose of the bus is to gather and integrate evidence for verification or refutation. In this paper I propose requirements for such an “evidential tool bus,” and sketch a possible architecture.

Although formal methods provide excellent techniques for the precise description of systems, understanding these descriptions is often restricted to experts. This paper investigates a practical solution to assist the understanding of a formal specification, written in B, by providing a complementary view of the specification as UML class diagram. Our technique improves the state of the art by taking into account operations in the construction of the diagram, through the use of concept formation techniques. A documentation tool automates the approach. It has been applied to several specifications built independently of the tool.

UML 2.0, which is the standard modeling language for object-oriented systems, has only an informally given semantics. This is in particular the case for UML 2.0 state machines, which are widely used for modeling the reactive behavior of objects. In this paper, a list of 29 newly detected trouble spots consisting of ambiguities, inconsistencies, and unnecessarily strong restrictions of UML 2.0 state machines is given and illustrated using 6 state machines having a problematic meaning; suggestions for improvement are presented. In particular, we show that the concepts of history, priority, and entry/exit points have to be reconsidered.

In this work, we firstly enhance OZTA, a combination of Object-Z and Timed Automata, by introducing a set of timed patterns as language constructs that can specify the dynamic and timing features of complex real-time systems in a systematic way. Then we present the formal semantics in Unifying Theories of Programming for the enhanced OZTA. Furthermore, we develop an OZTA tool which can support editing, type-checking of OZTA models as well as projecting OZTA models into TA models so that we can utilize TA model checkers, e.g., Uppaal for verification.

We define a high-level model to mathematically capture the behavioural interface of abstract Virtual Providers (VP), their refinements and their composition into rich mediator structures. We show for a Virtual Internet Service Provider example how to use such a model for rigorously formulating and proving properties of interest.

This paper presents a non-conventional application of symbolic animation. We propose to assist the modeller in building an efficient formal model, by automatically detecting potential weaknesses or imprecisions in the model. We propose to detect inconsistencies within the formal models written with pre- and postconditions, and to point out unusual model properties, such as a weak invariant or unreachable effects. Our approach is based on constraint solving technologies to perform the animation and to detect the various problems.

Control-Flow Integrity (CFI) means that the execution of a program dynamically follows only certain paths, in accordance with a static policy. CFI can prevent attacks that, by exploiting buffer overflows and other vulnerabilities, attempt to control program behavior. This paper develops the basic theory that underlies two practical techniques for CFI enforcement, with precise formulations of hypotheses and guarantees.

Our aim is to present a game semantics model for the specification of security protocols. Game semantics has been used to give an operational flavor to denotational semantics, thereby combining the best of both worlds by having an elegant mathematical structure and at the same time describing steps of execution. Game semantics was successfully used to prove full abstraction of PCF and has since been used to describe the semantics of a variety of programming languages. It fits naturally in the framework of security protocols as the interactions between communicating parties can be described as moves in a game, where honest agents are the players and the intruder is the opponent. We propose a game-based calculus for the specification of security protocols. First, we define games that represent interactions in security protocols, these games are then used to ascribe denotational semantics to security protocols.