Search

Decisions about the logic underpinning a formal specification language have important consequences for the utility of the formalism. This chapter describes the major features of the typed Logic of Partial Functions (LPF) as it has been implemented in support of the Vienna Development Method's Specification Language, VDM-SL. It compares attempts to realise the logic in different environments: a usercentred proof support tool, a specification interpreter and an automated proof tool. Future directions in integrated proof support for the language are suggested. [ABSTRACT FROM AUTHOR]

Our goal is to help the developers of computer-based systems to make informed design decisions on the basis of insights gained from the rigorous analysis of abstract system models. The early work on model-oriented specification has inspired the development of numerous formalisms and tools supporting modelling and analysis. There are also many stories of successful industrial application, often driven by a few champions possessing deep a priori understanding of formalisms. There are fewer cases of successful take-up or adoption of the technology in the long term. We argue that successful industrial adoption of this technology requires that potential users strike a balance between the effort expended in producing and analysing a model and insight gained. In order to support this balancing act, tools need to offer a range of levels of effort and insight. Further, educators need to recognise that training in formal development techniques must support this trade-off process. [ABSTRACT FROM AUTHOR]

This paper presents an innovative hybrid approach for online recognition of handwritten symbols. The approach is composed of two main techniques. Firstly, fuzzy rules are used to extract a meaningful set of features from a handwritten symbol, and secondly a recurrent neural network uses the feature set as input to recognise the symbol. The extracted feature set is a set of basic shapes capturing what is distinctive about each symbol, thus making the network's classification task easier. We propose a new recurrent neural network architecture, associated with an efficient learning algorithm derived from the gradient descent method. We describe the network and explain the relationship between the network and the Markov chains. The approach has achieved high recognition rates using benchmark datasets from the Unipen database. [ABSTRACT FROM AUTHOR]

This is a position paper about the relation between Formal Methods and Systems Engineering for complex computerized systems. We will argue that Formal Methods are well suited to prescribed homogeneous domains, and that systems engineering, which integrates more specialized engineering disciplines, is inherently much more informal. We will use the waferstepper as a typical complex computerized system, the case is described at the beginning. Next we explain the discipline of Systems Engineering. In a short intermezzo the overloaded meaning of the word "formal" is discussed. The real positioning is given in two steps: first we elaborate the informal nature of Systems Engineering and then we discuss the relation to Formal Methods. [ABSTRACT FROM AUTHOR]

We describe a practical model-based testing tool developed at Microsoft Research called Spec Explorer. Spec Explorer enables modeling and automatic testing of concurrent object-oriented systems. These systems take inputs as well as provide outputs in form of spontaneous reactions, where inputs and outputs can be arbitrary data types, including objects. Spec Explorer is being used daily by several Microsoft product groups. The here presented techniques are used to test operating system components and Web service infrastructure. [ABSTRACT FROM AUTHOR]

Software is now an essential component that is embedded in an ever-increasing array of products. It has become an important means of realising product innovation and is a key determinant of both product quality and time-to-market. For many businesses, software has become business-critical and software development is a strategic business activity. At the same time, software development continues to suffer from poor predictability. Existing development methods appear to have reached a quality ceiling that incremental improvements in process and technology are unlikely to breach. To break through this ceiling, a different, more formal approach is needed, but one which can be introduced within existing development organisations. [ABSTRACT FROM AUTHOR]

ProB is a model checking tool for the B Method. In this paper we present an extension of ProB that supports checking of specifications written in a combination of CSP and B. We explain how the notations are combined semantically and give an overview of the implementation of the combination. We illustrate the benefit that appropriate use of CSP, in conjunction with our tool, gives to B developments both for specification and for verification purposes. Keywords: B-Method, Tool Support, Model Checking, Animation, Logic Programming, Constraints. [ABSTRACT FROM AUTHOR]

Testing comprises activities that aim at showing that the intended and actual behaviors of a system differ, or at gaining confidence that they do not. The goal of testing is failure detection: observable differences between the behaviors of implementation and specification. Classical estimates relate one half of the overall development effort to testing. Even if Fagan [1] suspects that this percentage includes activities such as finding the causes of failures in the code and removing them, testing is an important and expensive activity in the development process. [ABSTRACT FROM AUTHOR]

Many safety-critical software applications are hard real-time systems. They have stringent timing requirements that have to be met. We present a description of timing behaviour that includes precise definitions as well as analysis of how functional timing requirements interact with performance timing requirements, and how these concepts can be used by software designers. The definitions and analysis presented explicitly deal with tolerances in all timing durations. Preliminary work indicates that some requirements may be met at significantly reduced CPU bandwidth through reduced variation in cycle time. Keywords:safety-critical, real-time, timing tolerances, requirements. [ABSTRACT FROM AUTHOR]

Model checking is a promising formal verification technique successfully applied in several industrial environments, such as in chip design and in the telecommunication industry. In this paper, preliminary results of an automotive case study are presented as performed in the context of the European project EASISEASIS - Electronic Architectures and System Engineering for Integrated Safety Systems - is partly funded by the European Commission under contract No IST-507690.. [ABSTRACT FROM AUTHOR]

Master/Slave Speculative Parallelization (MSSP) is a new execution paradigm that decouples the issues of performance and correctness in microprocessor design and implementation. MSSP uses a fast, not necessarily correct, master processor to speculatively split a program into tasks, which are executed independently and concurrently on slower, but correct, slave processors. This work reports on the first steps in our efforts to formally validate that overall correctness can be achieved in MSSP despite a lack of correctness guarantees in its performance-critical parts. We describe three levels of an abstract model for MSSP, each refining the next and each preserving equivalence to a sequential machine. Equivalence is established in terms of a jumping refinement, a notion we introduce to describe equivalence at specific places of interest in the code. We also report on experiences and insights gained from this exercise. In particular, we show how formalizing MSSP facilitated a deeper understanding of performance-correctness decoupling and its attendant trade-offs, all key features of the MSSP paradigm. Moreover, formalization revealed all assumptions underpinning correctness, which, being specified abstractly, can be understood in an implementation-independent way. We found these results so valuable that we plan to advance MSSP's formalization in parallel with its subsequent design iterations. [ABSTRACT FROM AUTHOR]

This paper presents a combination of verification and conformance testing techniques for the formal validation of reactive systems. A formal specification of a system, which may be infinite-state, and a set of safety properties are assumed. Each property is verified on the specification using automatic techniques based on abstract interpretation, which are sound, but, as a price to pay for automation, are not necessarily complete. Next, for each property, a test case is automatically generated from the specification and the property, and is executed on a black-box implementation of the system to detect violations of the property by the implementation and non-conformances between implementation and specification. If the verification step did not conclude, the test execution may also detect violations of the property by the specification. Keywords: verification, conformance testing, symbolic test generation [ABSTRACT FROM AUTHOR]

Only in a few isolated safety-critical niches of the software industry (e.g. avionics) is any kind of formal verification widespread. But in the hardware industry, formal verification is widely practised, and increasingly seen as necessary. We can perhaps identify at least three reasons: - Hardware is designed in a more modular way than most software, with refinement an important design method. Constraints of interconnect layering and timing means that one cannot really design ‘spaghetti hardware'. - More proofs in the hardware domain can be largely automated, reducing the need for intensive interaction by a human expert with the mechanical theorem-proving system. - The potential consequences of a hardware error are greater, since such errors often cannot be patched or worked around, and may in extremis necessitate a hardware replacement. [ABSTRACT FROM AUTHOR]

This paper presents an automated and compositional procedure to solve the substitutability problem in the context of evolving software systems. Our solution contributes two techniques for checking correctness of software upgrades: 1) a technique based on simultaneous use of over and under approximations obtained via existential and universal abstractions; 2) a dynamic assume-guarantee reasoning algorithm - previously generated component assumptions are reused and altered on-the-fly to prove or disprove the global safety properties on the updated system. When upgrades are found to be non-substitutable our solution generates constructive feedback to developers showing how to improve the components. The substitutability approach has been implemented and validated in the ComFoRT model checking tool set and we report encouraging results on an industrial benchmark. Keywords: Software Model Checking, Verification of Evolving Software, Learning Regular Sets, Assume/Guarantee Reasoning. [ABSTRACT FROM AUTHOR]

State space partitioning-based approaches have been proposed in the literature to address the state-space explosion problem in model checking. These approaches, whether sequential or distributed, perform a large amount of work in the form of inter-partition (cross-over) image computations, which can be expensive. We present a model checking algorithm that aggregates these expensive cross-over images by localizing computation to individual partitions. It reduces the number of cross-over images and drastically outperforms extant approaches in terms of cross-over image computation cost as well as total model checking time, often by two orders of magnitude. Keywords: Symbolic Model Checking, BDD, state partitioning, CTL. [ABSTRACT FROM AUTHOR]

We present an automatic technique for the detection of structural symmetry in a model directly from its Promela specification. Our approach involves finding the static channel diagram of the model, a graphical representation of channel-based system communication; computing the group of symmetries of this diagram; and computing the largest possible subgroup of these symmetries which induce automorphisms of the underlying model. We describe a tool, SymmExtractor, which, for a given model and LTL property, uses our approach to find a group of symmetries of the model which preserve the property. This group can then be used for symmetry reduction during model checking using existing quotient-based methods. Unlike previous approaches, our method can detect arbitrary structural symmetries arising from the communication structure of the model. Keywords: Promela /Spin; symmetry reduction; model checking; communicating processes; distributed systems; formal modelling; Gap; concurrency. [ABSTRACT FROM AUTHOR]

We present a new model-checking technique for CSP-OZ-DC, a combination of CSP, Object-Z and Duration Calculus, that allows reasoning about systems exhibiting communication, data and real-time aspects. As intermediate layer we will use a new kind of timed automata that preserve events and data variables of the specification. These automata have a simple operational semantics that is amenable to verification by a constraint-based abstraction-refinement model checker. By means of a case study, a simple elevator parameterised by the number of floors, we show that this approach admits model-checking parameterised and infinite state real-time systems. [ABSTRACT FROM AUTHOR]

The Model Driven Architecture (MDA) involves automated trans-formations between software models defined in different languages at different abstraction levels. This paper takes an MDA approach to integrate a formal modeling language (Object-Z) with an informal modeling language (UML) via model transformation. This paper shows how formal and informal modeling languages can be cooperatively used in the MDA framework and how the trans-formations between models in these languages can be achieved using an MDA development environment. The MDA model transformation techniques allow us to have a reusable transformation between formal and informal modeling languages. The integrated approach provides an effective V&V technique for the MDA. [ABSTRACT FROM AUTHOR]

Software systems specifications are often described as a set of typical scenarios. Some of the desired scenarios are crosscut by other requirements, called aspects, also naturally described as scenarios. Aspect descriptions are independent of the description of the non-aspectual scenarios, but the crosscutting relationship between them has to be specified, so for each aspect a description of its join-points is provided. When aspectual scenarios are added to the system, we need to prove that every execution is equivalent to one in which the aspectual scenarios occur as blocks of operations immediately at their join-points, and all the other operations form a sequence of non-aspectual scenarios, interrupted only by the aspectual scenarios. We extend an existing method of automatic verification for non-aspect systems to the case of systems with scenario-based aspect specifications. A prototype implementation based on Cadence SMV is also extended accordingly. Keywords: Aspects, scenarios, model-checking, conformance, convenient executions. [ABSTRACT FROM AUTHOR]

Given a set of sequence diagrams, the problem of synthesis is of deciding whether there exists a satisfying object system and if so, synthesize one automatically. It is crucial in the development of complex systems, since sequence diagrams serve as the manifestation of use cases and if synthesizable they could lead directly to implementation. It is even more interesting (and harder) if the synthesized object system is distributed. In this paper, we propose a systematic way of synthesizing distributed processes from Live Sequence Charts. The basic idea is to first construct a CSP specification from the LSC specification, and then use CSP algebraic laws to group the behaviors of each object effectively. The key point is that the behaviors of each object can be decided locally without constructing the global state machine. Keywords: LSC, CSP, Synthesis. [ABSTRACT FROM AUTHOR]

We constructed a tool, called VooDooM, which converts datatypes in Vdm-sl into Sql relational data models. The conversion involves transformation of algebraic types to maps and products, and pointer introduction. The conversion is specified as a theory of refinement by calculation. The implementation technology is strategic term rewriting in Haskell, as supported by the Strafunski bundle. Due to these choices of theory and technology, the road from theory to practise is straightforward. Keywords: Strategic term rewriting, program calculation, Vdm, Sql. [ABSTRACT FROM AUTHOR]

The Mondex Electronic Purse system [18] is an outstanding example of formal refinement techniques applied to a genuine industrial scale application, and notably, was the first verification to achieve ITSEC level E6 certification. A formal abstract model including security properties, and a formal concrete model of the system design were developed, and a formal refinement was hand-proved between them in Z. Despite this success, certain requirements issues were set beyond the scope of the formal development, or handled in an unnatural manner. Retrenchment is reviewed in a form suitable for integration with Z refinement, and is used to address one such issue in detail: the finiteness of the transaction sequence number in the purse funds transfer protocol. A retrenchment is constructed from the lowest level model of the purse system to a model in which sequence numbers are finite, using a suitable elaboration of the Z promotion [21] technique. We overview the lifting of that retrenchment to the abstraction level of the higher models of the purse system. The concessions of the various retrenchments generated, formally capture the dissonance between the unbounded sequence number idealisation and the bounded reality. Reasoning about when the concession can become valid influences the actual choice of sequence number bound. The retrenchment-enhanced formal development is proposed as an example of a widely applicable methodological pattern for formal developments of this kind: the Tower Pattern. [ABSTRACT FROM AUTHOR]

In this paper we give some abstractions that preserve sublanguages of the universal part of the branching-time μ-calculus Lμ. We first extend some results by Loiseaux et al. by using a different abstraction for the universal fragments of Lμ which are treated in their work. We show that this leads to a more elegant theoretical treatment and more practical verification methodology. After that, we define an abstraction for a universal fragment of Lμ in which the formulas can contain the -operator only under an even number of negations. The abstraction we propose is inspired by the work of Loiseaux et al., and Kesten and Pnueli. From the former we use the approach based on Galois connections, while from the latter we borrow the idea of "rewriting" the original formula using contracting/expanding abstractions. We argue that, besides removing some unnecessary syntactic restrictions, our approach leads to more compact and practical solutions to the abstraction problems. Keywords: abstraction, property preservation, mu-calculus, model checking. [ABSTRACT FROM AUTHOR]

BPEL4WS is one of the most important business process modelling languages. One distinct feature of it is the fully programmable fault and compensation handling mechanism, which allows the user to specify the compensation behaviors of processes in application-specific manners. In this paper, we present a formal operational semantics to a simplified version of BPEL4WS, with some important concepts related to fault and compensation handling proposed and discussed, especially, the compensation closure and the compensation context. We also discuss some insights into the BPEL4WS language and its implementation obtained from this study. Keywords: Business Process, Language, Semantics, BPEL4WS, Compensation handling, Fault handling. [ABSTRACT FROM AUTHOR]

We present an approach to directly unfold asynchronous communication protocols that are modeled as a group of Extended Finite State Machines (EFSMs) communicating through shared message queues. A novel aspect of our approach is that we reduce the redundancy in representing the states of message queues by storing individual messages separately in our unfolding representation. Our approach can also take advantage of the compositional nature of these protocols to minimize the size of a complete finite prefix of their potentially infinite unfoldings. Our empirical results indicate that our approach can produce very compact state space representations. Keywords: Software Verification, State Space Search, Unfolding, EFSM. [ABSTRACT FROM AUTHOR]

This paper reports on a method to handle the verification of various security properties of imperative source code embedded on smart cards. The idea is to combine two program verification approaches: the functional verification at the source code level and the verification of high level properties on a formal model built from the program and its specification. The method presented uses the Caduceus tool, built on top of the Why tool. Caduceus enables the verification of an annotated C program and provides a validation process that we used to generate a high level formal model of the C source code. This method is illustrated by an example extracted from the verification of a smart card embedded operating system. Keywords: Theorem Proving, Smart Card, Security, Source code verification, Formal Methods. [ABSTRACT FROM AUTHOR]

Designing network address spaces for interoperation among domains is a challenging task. A formal model in Alloy is used to clarify the problems and explore solutions. Basic connectivity requirements are proposed, and two different sets of constraints are shown to satisfy them. Keywords: networks, network design, network requirements, Alloy. [ABSTRACT FROM AUTHOR]

We present a software tool platform which facilitates security and performance analysis of systems which starts and ends with UML model descriptions. A UML project is presented to the platform for analysis, formal content is extracted in the form of process calculi descriptions, analysed with the analysers of the calculi, and the results of the analysis are reflected back into a modified version of the input UML model. The design platform supporting the methodology, Choreographer, interoperates with state-of-the-art UML modelling tools. We illustrate the approach with a well known protocol and report on the experience of industrial users who have applied Choreographer in their development work. Keywords: security analysis, performance analysis, process calculi, UML. [ABSTRACT FROM AUTHOR]

We report on a case study in using HOL-Z, an embedding of Z in higher-order logic, to specify and verify a security architecture for administering digital signatures. We have used HOL-Z to formalize and combine both data-oriented and process-oriented architectural views. Afterwards, we formalized temporal requirements in Z and carried out verification in higher-order logic. The same architecture has been previously verified using the SPIN model checker. Based on this, we provide a detailed comparison of these two different approaches to formalization (infinite state with rich data types versus finite state) and verification (theorem proving versus model checking). Contrary to common belief, our case study suggests that Z is well suited for temporal reasoning about process models with rich data. Moreover, our comparison highlights the advantages of this approach and provides evidence that, in the hands of experienced users, theorem proving is neither substantially more time-consuming nor more complex than model checking. [ABSTRACT FROM AUTHOR]

Control diagrams are routinely used by engineers in the design of control systems. Yet, currently the formal verification of programs that implement the diagrams is a challenge. We present a strategy to translate block diagrams to Circus, a notation that combines Z, CSP, and a refinement calculus. This work is based on existing tools that produce Z and CSP specifications from discrete-time block diagrams. By using a combined notation, we provide a specification that considers both functional and behavioural aspects of these diagrams, and can cover a wider range of blocks. Moreover, the Circus refinement calculus can be used to verify implementations, and reason about the block diagrams. Keywords: Z, CSP, Simulink, refinement. [ABSTRACT FROM AUTHOR]

Circus is a combination of Z, CSP, and the refinement calculus, and is based on Hoare & He's Unifying Theories of Programming. A model checker is being constructed for the language to conduct refinement checking in the style of FDR, but supported by theorem proving for reasoning about the complex states and data types that arise from the use of Z. FDR deals with bounded labelled transition systems (LTSs), but the Circus model checker manipulates LTSs with possibly infinite inscriptions on arcs and in nodes, and so, in general, the success or failure of a refinement check depends on interaction with a theorem prover. An LTS is generated from a source text using an operational interpretation of Circus; we present a Structured Operational Semantics for Circus, including both its process-algebraic and state-rich features. [ABSTRACT FROM AUTHOR]

In the development of concurrent systems two differing approaches have arisen: those with truly concurrent semantics and those with interleaving semantics. The difference between these two approaches is that in the coarser interleaving interpretation parallelism can be captured in terms of non-determinism whereas in the finer truly concurrent interpretation it cannot. Thus processes a ∥ b and a.b + b.a are identified within the interleaving approach but distinguished within the truly concurrent approach. In this paper we explore the truly concurrent notions of conflict, whereby transitions can occur individually but not together from a given state, and confusion, whereby the conflict set of a given transition is altered by the occurrence of another transition with which it does not interfere. Having provided a translation from Petri nets, a truly concurrent formalism, to CSP, an interleaving formalism, we demonstate how the CSP model-checker FDR can be used to detect the presence of both conflict and confusion in Petri nets. This work is of interest for two reasons. Firstly, from a practical point of view: to the author's knowledge, no existing tool for modelling Petri nets can perform these checks and we address that issue. Secondly, and perhaps more significantly, we bridge the gap between truly concurrent and interleaving formalisms, demonstrating that true concurrency can be captured in what is typically considered to be an interleaving language. Keywords: True Concurrency; Interleaving Concurrency; Petri Nets; CSP; Conflict; Confusion; Automatic Verification. [ABSTRACT FROM AUTHOR]

Recently we have proposed the "almost ASAP" semantics as an alternative semantics for timed automata. This semantics is useful when modeling real-time controllers : control strategies modeled with this semantics are robust and implementable (without making the synchrony hypothesis). We show in this paper how to effectively encode this semantics using timed automata along with their classical semantics. We have implemented a tool set that allows us to verify, using HyTech and Uppaal, the almost ASAP behavior of controllers and generate automatically provably correct code from verified models. To illustrate the applicability of our results, we show how we have synthesized the code for the Philips Audio Control Protocol for Lego MindstormsTM. [ABSTRACT FROM AUTHOR]

TorX is a specification-based, on-the-fly testing tool that tests for ioco conformance of implementations w.r.t. a formal specification. This paper describes an extension of TorX to not only allow testing for functional correctness, but also for correctness w.r.t. timing properties expressed in the specification. An implementation then passes a timed test if it passes according to ioco, and if occurrence times of outputs or of quiescence signals are legal according to the specification. The specifications are described by means of non-deterministic safety timed automata. This paper describes the basic algorithms for ioco, the necessary modifications to standard safety timed automata to make them usable as an input formalism, a test-derivation algorithm from timed automata, and the concrete algorithms implemented in TorX for timed testing. Finally, practical concerns with respect to timed testing are discussed. Keywords: Model-based on-the-fly Testing, Timed Automata, Real-Time Testing, TorX, Tools. [ABSTRACT FROM AUTHOR]

We present a certified algorithm for resource usage analysis, applicable to languages in the style of Java byte code. The algorithm verifies that a program executes in bounded memory. The algorithm is destined to be used in the development process of applets and for enhanced byte code verification on embedded devices. We have therefore aimed at a low-complexity algorithm derived from a loop detection algorithm for control flow graphs. The expression of the algorithm as a constraint-based static analysis of the program over simple lattices provides a link with abstract interpretation that allows to state and prove formally the correctness of the analysis with respect to an operational semantics of the program. The certification is based on an abstract interpretation framework implemented in the Coq proof assistant which has been used to provide a complete formalisation and formal verification of all correctness proofs. Keywords: Program analysis, certified memory analysis, theorem proving, constraint solving. [ABSTRACT FROM AUTHOR]

Sharing of objects between different modules is often necessary to meet speed and resource demands. The invariants that describe properties of shared objects are difficult to maintain because they can be falsifiable by object allocation. This paper introduces creation guards to obtain a sound and modular methodology that supports such invariants. Keywords:invariants, object allocation, specification, verification, object-oriented programming. [ABSTRACT FROM AUTHOR]

We introduce a formal framework for reasoning about performance-style properties of probabilistic programs at the level of program code. Drawing heavily on the refinement-style of program verification, our approach promotes abstraction and proof re-use. The theory and proof tools to facilitate the verification have been implemented in HOL. [ABSTRACT FROM AUTHOR]

This paper presents a model-based framework for the symbolic animation of object-oriented specifications. A customized set-theoretic solver is used to simulate the execution of the system and handle constraints on state variables. We define a framework for animating object-oriented specifications with dynamic object creations, interactions and inheritance. We show how this technique can be applied to Java Modeling Language (JML) specifications, making it possible to animate Java programs that only contain method interfaces and no code! Keywords: Java Modeling Language, JML, model-based, object-oriented, symbolic animation. [ABSTRACT FROM AUTHOR]

In formal design, decoupling means to make the features of a formal system as independent as possible from each other. Decoupling tends to make the features semantically more primitive and the overall system more general. Quite opposite to decoupling, the tradition in object oriented refinement theories is to combine all features, such as specification, usage constraints, encapsulation and inheritance into a single formal construct, the class. We propose a decoupled formalization of object orientation, in which all those features are introduced independently from the class construct and from each other. Even though each of the features is significantly simpler than its standard counterparts, the overall system is more general: standard class-based object orientation is shown to be a special case of our system. Keywords: object orientation, specification and refinement [ABSTRACT FROM AUTHOR]

Object invariants describe the consistency of object-oriented data structures and are central to reasoning about the correctness of object-oriented software. But object invariants are not the only consistency conditions on which a program may depend. The data in object-oriented programs consists not just of object fields, but also of static fields, which hold data that is shared among objects. The consistency of static fields is described by static class invariants, which are enforced at the class level. Static class invariants can also mention instance fields, describing the consistency of dynamic data structures rooted in static fields. Sometimes there are even consistency conditions that relate the instance fields of many or all objects of a class; static class invariants describe these relations, too, since they cannot be enforced by any one object in isolation. This paper presents a systematic way (a methodology) for specifying and verifying static class invariants in object-oriented programs. The methodology supports the three major uses of static fields and invariants in the Java library. The methodology is amenable to static, modular verification and is sound. Keywords: Static class invariant, verification, object-oriented programming, static field. [ABSTRACT FROM AUTHOR]

Space missions force engineers to make complex trade-offs between many different constraints including cost, mass, power, functionality and reliability. These constraints create a continual need to innovate. Many advances rely upon software, for instance to control and monitor the next generation ‘electron cyclotron resonance' ion-drives for deep space missions.Programmers face numerous challenges. It is extremely difficult to conduct valid ground-based tests for the code used in space missions. Abstract models and simulations of satellites can be misleading. These issues are compounded by the use of ‘band-aid' software to fix design mistakes and compromises in other aspects of space systems engineering. Programmers must often re-code missions in flight. This introduces considerable risks. It should, therefore, not be a surprise that so many space missions fail to achieve their objectives. The costs of failure are considerable. Small launch vehicles, such as the U.S. Pegasus system, cost around $18 million. Payloads range from $4 million up to $1 billion for security related satellites. These costs do not include consequent business losses. In 2005, Intelsat wrote off $73 million from the failure of a single uninsured satellite. It is clearly important that we learn as much as possible from those failures that do occur. The following pages examine the roles that formal methods might play in the analysis of software failures in space missions. [ABSTRACT FROM AUTHOR]

It has been recognised for a while that formal specifications can bring much to software testing. Numerous methods have been proposed for the derivation of test cases from various kinds of formal specifications, their submission, and verdict. All these methods rely upon some hypotheses on the system under test that formalise the gap between the success of a test campaign and the correctness of the system under test. [ABSTRACT FROM AUTHOR]

The use of formal techniques has for a long time been focused on relatively small and complex applications. The hardware domain lends itself well to this and it has therefore been the target of some of the most significant applications of formal techniques. The software applications that have typically been considered were for small, safety-critical systems. This restricted focus was understandable and necessary while formal techniques were evolving and practical considerations limited the size of the system that could be specified and verified. However, there are now compelling demands for the use of more precise techniques for a variety of large-scale applications, ranging from smart cards to financial systems. So there are now new reasons to extend the use of formal methods for all phases of software development: from requirements and software modeling to coding and testing. Problems of scale still remain so it is important to focus the use of formal techniques in areas where their impact will be most important. Different formal techniques can be used for solving different problems. For example, use of model-checking during requirements modeling can identify incomplete or inconsistent specifications, while use of transformational techniques can be very effective for software modeling and enable generation of code directly from models. Program analysis techniques can be used to generate tests that will greatly improve functional coverage during testing. The use of formal techniques continues during software maintenance through the following kinds of activities: a. Remedial: correction of errors discovered during use; b. Adaptive: making changes to cater to changes in the operating environment; c. Enhancing: adding new features or capabilities; and d. Improving: making the software more robust and easier to maintain. It is estimated that the cost of software maintenance amounts to as much as 90% of the life-cycle cost of a software system. While this calls for major improvements in maintenance techniques, changes in software development methods can also help to reduce the need for, and therefore the cost of, making remedial improvements (i.e. bug fixing). In this talk, I will describe the use of formal techniques for different areas of the software life-cycle and relate this to evidence obtained through the analysis of a large number of actual software development and maintenance projects. [ABSTRACT FROM AUTHOR]