nach oben

2010 | Buch

Formal Methods: State of the Art and New Directions

herausgegeben von: Paul Boca, Jonathan P. Bowen, Jawed Siddiqi

Verlag: Springer London

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Inhaltsverzeichnis

Frontmatter

1. Domain Engineering

Abstract

Before software can be designed we must know its requirements. Before requirements can be expressed we must understand the domain. So it follows, from our dogma, that we must first establish precise descriptions of domains; then, from such descriptions, “derive” at least domain and interface requirements; and from those and machine requirements design the software, or, more generally, the computing systems.

Dines Bjørner

2. Program Verification and System Dependability

Abstract

Formal verification of program correctness is a long-standing ambition, recently given added prominence by a “Grand Challenge” project. Major emphases have been on the improvement of languages for program specification and program development, and on the construction of verification tools. The emphasis on tools commands general assent, but while some researchers focus on narrow verification aimed only at program correctness, others want to pursue wide verification aimed at the larger goal of system dependability. This paper presents an approach to system dependability based on problem frames and suggests how this approach can be supported by formal software tools. Dependability is to be understood and evaluated in the physical and human problem world of a system. The complexity and non-formal nature of the problem world demand the development and evolution of normal designs and normal design practices for specialised classes of systems and subsystems. The problem frames discipline of systems analysis and development that can support normal design practices is explained and illustrated. The role of formal reasoning in achieving dependability is discussed and some conceptual, linguistic and software tools are suggested.

Michael Jackson

3. The Abstract State Machines Method for High-Level System Design and Analysis

Abstract

We explain the main ingredients of the Abstract State Machines (ASM) method for high-level system design and analysis and survey some of its application highlights in industrial software-based system engineering. We illustrate the method by defining models for three simple control systems (sluice gate, traffic light, package router) and by characterising Event-B machines as a specific class of ASMs.We point to directions for future research and applications of the method in other areas than software engineering.

Egon Börger

4. Applications and Methodology of νZ

Abstract

In this chapter, we describe a specification logic called νZ. This is a Z-like formal method in which specifications are theories, not simply definitions. We examine simple applications and discuss some methodological issues that these illustrate. The chapter is introductory, and should be comprehensible to a reader with a knowledge of predicate logic and some familiarity with the ideas of computer system specification.

Martin C. Henson

5. The Computer Ate My Vote

Abstract

Public confidence in voting technologies has been badly shaken over the past years by, amongst other events, the problems with the 2000 and 2004 US presidential elections and the 2007 French presidential election. Serious vulnerabilities have been exposed and documented in all the existing electronic voting systems. Many of these systems use proprietary, protected code and the voters and election officials are expected to take assurances of the suppliers and certifiers on trust.

In the face of this, many activists argue that all voting systems employing information technology in place of humans to process the votes must be flawed and we should return to pen-and-paper along with hand counting. The critiques of existing voting technologies are undoubtedly well-founded, but to infer from this that all technology must be flawed is an elementary error of logic. In this chapter, I present an alternative response and describe schemes that derive their trustworthiness from maximal transparency and auditability.

Designing voting systems that provide high levels of assurance of accuracy and ballot secrecy with minimal trust assumptions is an immensely challenging one. The requirements of accuracy and auditability are in direct conflict with those of ballot secrecy. A voting system must deliver high assurance of accuracy and privacy in a highly hostile environment: the system may try to cheat the voters, voters may try to circumvent the system, officials may try to manipulate the outcome and coercers may attempt to influence voters. Furthermore, we must recognise that this is not a purely technical problem: a technically perfect solution that is not usable or does not command the confidence of the voters is not a viable solution.

Recently significant progress has been made and a number of schemes developed that provide verifiability of the election. These seek to provide end-to-end verifiability of the outcome, i.e., the accuracy of the outcome is independent of the code or hardware that implements the ballot processing. The assurance is derived from maximal transparency and auditability. Voters are provided with mechanisms to check that their vote is accurately included in the final tally, all the while maintaining ballot secrecy. Thus, the assurance depends ultimately on the voters rather than the probity of election officials, suppliers of voting systems, etc.

In this chapter, I describe the requirements for voting systems, the required cryptographic building blocks and a variety of threats they have to deal with. I then describe the Prêt à Voter scheme, a particularly voter-friendly example of a voter-verifiable, high assurance scheme. I also describe a number of enhancements to the basic scheme that are designed to counter those threats to which the basic version of Prêt à Voter is potentially vulnerable.

Peter Y.A. Ryan

6. Formal Methods for Biochemical Signalling Pathways

Abstract

We apply quantitative formal methods to a domain from the life sciences: biochemical signalling pathways. The key idea is to model pathways as stochastic continuous time distributed systems. Components of the system are molecular species (rather than individual molecules) and are modelled by concurrent processes that interact with each other via biochemical reactions. Through an application, we show how high level languages and analysis techniques rooted in computer science theory add significantly to the analysis presently available to computational biologists.

Muffy Calder, Stephen Gilmore, Jane Hillston, Vladislav Vyshemirsky

7. Separation Logic and Concurrency

Abstract

Concurrent separation logic is a development of Hoare logic adapted to deal with pointers and concurrency. Since its inception, it has been enhanced with a treatment of permissions to enable sharing of data between threads, and a treatment of variables as resource alongside heap cells as resource. An introduction to the logic is given with several examples of proofs, culminating in a treatment of Simpson’s 4-slot algorithm, an instance of racy non-blocking concurrency.

Richard Bornat

8. Programming Language Description Languages

From Christopher Strachey to Semantics Online

Abstract

Since the middle of the twentieth century, hundreds of programming languages have been designed and implemented – and new ones are continually emerging. The syntax of a programming language can usually be described quite precisely and efficiently using formal grammars. However, the formal description of its semantics is much more challenging. Language designers, implementers and programmers commonly regard formal semantic descriptions as impractical. Research in semantics has allowed us to reason about software and has provided valuable insight into the design of programming languages, but few semantic descriptions of full languages have been published, and hardly any of these are currently available online.

One of the major approaches to formal semantics is denotational semantics, which originated from Strachey’s pioneering studies in the 1960s. Why is such a theoretically attractive approach generally regarded as impractical for describing full-scale programming languages? Does it help much to use monads in denotational descriptions, or is a more radical change needed? How might efficient online access to a repository of semantic descriptions be provided? Could it ever become as easy to generate efficient compilers and interpreters from semantic descriptions as it already is to generate parsers from grammars? This chapter addresses such questions and gives some grounds for optimism about the development of highly practical, online semantic descriptions.

Peter D. Mosses

Titel: Formal Methods: State of the Art and New Directions
herausgegeben von: Paul Boca
Jonathan P. Bowen
Jawed Siddiqi
Verlag: Springer London
Electronic ISBN: 978-1-84882-736-3
Print ISBN: 978-1-84882-735-6
DOI: https://doi.org/10.1007/978-1-84882-736-3

Springer Professional

Inhaltsverzeichnis

Frontmatter

1. Domain Engineering

2. Program Verification and System Dependability

3. The Abstract State Machines Method for High-Level System Design and Analysis

4. Applications and Methodology of νZ

5. The Computer Ate My Vote

6. Formal Methods for Biochemical Signalling Pathways

7. Separation Logic and Concurrency

8. Programming Language Description Languages

Premium Partner