This text is a companion to the lecture Formal Specification and Verification (FSV) as part of the master program High Integrity Systems (HIS). It is intended for students with basic knowledge in computer science and/ or engineering and it is formatted for a 1-semester course. This text will and cannot replace the texts mentioned below. Rather it is a 'guide' to use these books for a course with limited scope.
As primary textbooks we will use in this course Baier et al. (2008)[28], Berard et al (2001)[34], Clarke et al. (1999)[61], as well as Schneider (2004)[250]. Other very helpful books are those from McMillan (1993)[196], Manna and Pnueli (1992)[191] and (1995)[192] as well as Girault and Valk (2003). [116].
One has to keep in mind that a complete and deep unerstanding of the subject is only possible if one reads also the original papers cited in the books. The books can only give first ideas and represent selections of some perspectives.
Here is a short historical overview of the development of some of the topics which are important for the field (cf. figure 1.1):
Figure 1.1:
A simple overview about the topic formal specification and verification
|
- E. M. Clarke, E. A. Emerson, A. P. Sistla (1983, 1986)[65], [64]) introduced the branching time logic CTL as specification language to describe properties of finite-state concurrent programs together with a model checking algorithm. Indeed it is a slightly extended CTL called FCTL or CTL. This allowed the verification of some fairness properties in linear time. In contrast has the checking algorithm for a linear-time logic like LTL PSPACE-complexity. Important is here, that the authors already built the fairness conditions into the semantics of CTL, especially into the concept of a fair path!
- E. A. Emerson and Ch-L.Lei (1985) [96] use the results of Clarke et al. from 1983 but convert the behavior of the finite-state concurrent programs in a way that they can use the propositional My-Calculus for verification. The group Burch, J.R., E.M.Clarke, K.L.McMillan, D.L.Dill and L.J.Hwang continued (1990)[50] with the work in the way that they used as specification language the My Calculus combined with the BDD Technique of R.E. Bryant and they showed how one can reframe several decision procedures in this framework (CTL model checking, satisfiability of LTL, strong and week observational equivalence, and language containement for finite -automata).
- R.E.Bryant (1986) [47] introduces a new concept how to represent the structures of the execution graphs (often modeled as Kripke structures) as binary decision diagrams, BDDs. This technique allows a kind of symbolic model checking and enhances the applicability of model checking remarkably. Following the idea of R.E.Bryant do Fujita, M, Fujisawa, H., and Kawato, N. (1988)[105] improve the ordering mechanism for the variables in the BDD algorithm. Another efficient Implementation of a BDD package is reproted by Brace, K.S.; Rudell, R.L. and Bryant, R.E. (1990)[45]. Later, 1991, R.E.Bryant [46] publishes some results about the complexity of VLSI Implementations compared to OBDDs.
- 1986: C.Courcoubetis, M.Y.Vardi and P.Volper (1986) [72] investigate the application of branching time logic (BTL) like CTL and CTL on a general fairness condition which is assumed to be an integral part of the computations and not of the specification language. For the decision procedure of fair programs they use Büchi-Automata on infinite trees. Emerson and Halpern [95] introduce the more geneal language CTL to compare the power of LTL and CTL.: ``The differences between and appropriateness of branching versus linear time temporal logic for reasoning about concurrent programs are studied. These issues have been previously considered by Lamport. To facilitate a careful examination of these issues, a language, CTL*, in which a universal or existential path quantifier can prefix an arbitrary linear time assertion, is defined. The expressive power of a number of sublanguages is then compared. CTL* is also related to the logics MPL of Abrahamson and PL of Harel, Kozen, and Parikh. The paper concludes with a comparison of the utility of branching and linear time temporal logics''. Clarke et. [64] give an efficient procedure for verifying that a finite-state concurrent system meets a specification expressed in a (propositional, branching-time) temporal logic. The used algorithm has complexity linear in both the size of the specification and the size of the global state graph for the concurrent system. They also show how this approach can be adapted to handle fairness.
- Faced with the state-explosion problem where one has to deal with a system of N-many processes E. M. Clarke and O.Grumberg (1987) [63] develop the idea to partition the processes into small numbers of equivalence classes and try by this procedure to reduce the amount of states. The paper describes this interesting idea without having this idea implemented as software.
- To be able to specify properties of concurrnt processes with a variable number N of processes E. A. Emerson and J.Srinivasan (1990) [93] develop the concept of an indexed simplyfied CTL, indexed SCTL. The goal is to support the mechanical synthesis of programs based on specifications. In this context there is also a paper of E. A. Emerson and S.Jutla (1990) [93] about the complexity to test the nonemptiness of finite state automata on infinite trees. In another paper show E. A. Emerson and C.S.Jutla (1990)[94] that one can replace the structure of finite automata on infinite trees with the propositional Mu Calculus. This allows a drastically simplification of a proof of Rabin from 1969 and it allows the establishment of the determinacy of infinite games.
- In 1990 Alur, R., Courcoubetis, C., and Dill, D. [16] publish a paper where they extend the CTL specifications to the domain of dense time processes. They extend the CTL-Specification language to TCTL. Instead of implicitly integer based time domains which have monotonic evenly spaced distances they introduce dense time based continuous computation trees. Similar publish Wong-Toi, H.; Hoffmann, G.(1991) [297] first results about timed automata to control discrete event-systems with dense real-time. These considerations are continued by Henzinger, T.A.; Nicollin, X.; Sifakis, J.; Yovine, S. (1992)[125] using finite automata, BDDs, dense time, timed CTL, and mu calculus. Another paper here is that of Alur, R. and Dill, D.L.(1994)[13] in their lengthy paper about a theory of timed automata. From another perspective do R. Alur, C. Courcoubetis, T.A. Henzinger (1994) [12] investigate the possibility to distinguish different real time system from the point of an observer (untimed, clocked, timed). Furthermore did R. Alur and T.A. Henzinger (1994)[11] some research with real-time systems using timed PTL (TPTL) as specification language and as well the investigation into event clock automata by R. Alur, L. Fix, T.A. Henzinger (1994)[10]. This is a very interesting class of automata, which also can be used as specification language. In this context belongs also the the case study of Heitmeyer, C.; Lynch, N.(1994)[123] giving a generalized railroad crossing example with timed automata. Another research paper with timed automata is from R. Alur, C. Coucoubetis, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine (1995)[8]. A case study for the Automatic symbolic verification of embedded systems is 1996 be presented by R. Alur, T.A. Henzinger, P.-H. Ho[7]. An interesting topic is too to verify Abstractions of Timed Systems as developed by Tasiran, S. et al. (1996)[271]. Another case study is given 1997 by R. Alur, L.J. Jagadeesan, J.J. Kott, and J.E. Von Olnhausen [6]. Kowalewski, S. et al.did 1997[160] investigate, how it is possible to translate function blocks into real-time automata. As software tool do they use Kronos. In 1998 introduced Yamane, S. [299] the idea, to use a Hierarchical design method for real-time distributed systems. Another new idea has been proposed 1999 by Bultan, T.; Gerber, R.; Pugh, W.[48] to Model-check concurrent systems with infinite state sets with unbounded integer variables: symbolic representations, approximations, and encouraging experimental results.
- 1992 publish E. M. Clarke, O. Grumberg, D.Long [62] a lengthy research report about model checking, which gives a good overview of the subject.
- 1997: Asarin, E.; Caspi, P.; Maler, O.[21] did an investigation in the timed regular languages and show that these are equivalent to the timed automata from Alur and Dill. In this year published Heljanko, K.[124] his PhD thesis about model checking the Branching Time Temporal Logic CTL, with a lot of new algorithms.
- 1999: Norström, Chr.; Wall, A.; Yi, W. propose the idea to reconstruct the scheduling problem of real-time systems as timed automata, where the transitions are extended with tasks, which can be periodic or aperiodic. The schedulability problem can then be turned into a reachability problem, which is decidable. This allows the application of model-checking tools to schedulability analysis. The authors use the model-checker tool UPPAAL. Biere et al. [36] show a new approach of model checking optimization without BDDs: ``In this paper, we study the application of propositional decision procedures in hardware veri?cation. In particular, we apply bounded model checking to equivalence and invariant checking. We present several optimizations that reduce the size of generated propositional formulas. In many instances, our SAT-based approach can signi?cantly outperform BDD-based approaches. We observe that SAT-based techniques are particularly ef?cient in detecting errors in both combinational and sequential designs.''
- In 2000 Bellini et al. [33] contribute a large paper about ``Temporal Logics for Real-Time System Specification''. They write ``The specification of reactive and real-time systems must be supported by formal, mathematically-founded methods in order to be satisfactory and reliable. Temporal logics have been used to this end for several years. Temporal logics allow the specification of system behavior in terms of logical formulas, including temporal constraints, events, and the relationships between the two. In the last ten years, temporal logics have reached a high degree of expressiveness. Most of the temporal logics proposed in the last few years can be used for specifying reactive systems, although not all are suitable for specifying real-time systems. In this paper we present a series of criteria for assessing the capabilities of temporal logics for the
specification, validation, and verification of real-time systems. Among the criteria are the logic's expressiveness, the logic's order, presence of a metric for time, the type of temporal operators, the fundamental time entity, and the structure of time. We examine a selection of temporal logics proposed in the literature. To make the comparison clearer, a set of typical specifications is identified and used with most of the temporal logics considered, thus presenting the reader with a number of real examples.'' In the same year Kupferman et al [180] contribute a lengthy paper An automata-theoretic approach to branching-time model checking. They write: Translating linear temporal logic formulas to automata has proven to be an effective approach for implementing linear-time model-checking, and for obtaining many extensions and improvements to this verification method. On the other hand, for branching temporal logic, automata-theoretic techniques have long been thought to introduce an exponential penalty, making them essentially useless for model-checking. Recently, Bernholtz and Grumberg [1993] have shown that this exponential penalty can be avoided, though they did not match the linear complexity of non-automata-theoretic algorithms. In this paper, we show that alternating tree automata are the key to a comprehensive automata-theoretic framework for branching temporal logics. Not only can they be used to obtain optimal decision procedures, as was shown by Muller et al., but, as we show here, they also make it possible to derive optimal model-checking algorithms. Moreover, the simple combinatorial structure that emerges from the automata-theoretic approach opens up new possibilities for the implementation of branching-time model checking and has enabled us to derive improved space complexity bounds for this long-standing problem.
- 2001: Attie, P.C. and Emerson, E.A. improved the methods [25] automatically to synthesize concurrent programs for an atomic read/write model of computation. Huuck et al. [139] combined two different approaches for the specification and verification of timed systems being used in control theory and computer science. These are the timed condition/event systems and the timed automata formalisms. Their main result states that timed condition/event systems can be efficiently transformed into timed automata which then can be analyzed automatically.
- 2002: Besides linear temporal logic and branching time logic do Alur, R.; Henzinger, T.A. and Kupferman, O. 2002 introduce a third type of temporal logic: Alternating-time temporal logic. This logic is e.g. connected to an application in the domain of concurrent games: Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by the execution of a system; branching-time temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternating-time temporal logic offers selective quantification over those paths that are possible outcomes of games, such as the game in which the system and the environment alternate moves. While linear-time and branching-time logics are natural specification languages for closed systems, alternating-time logics are natural specification languages for open systems. For example, by preceding the temporal operator "eventually" with a selective path quantifier, we can specify that in the game between the system and the environment, the system has a strategy to reach a certain state. The problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas. Depending on whether or not we admit arbitrary nesting of selective path quantifiers and temporal operators, we obtain the two alternating-time temporal logics ATL and ATL. ATL and ATL are interpreted over concurrent game structures. Every state transition of a concurrent game structure results from a choice of moves, one for each player. The players represent individual components and the environment of an open system. Concurrent game structures can capture various forms of synchronous composition for open systems, and if augmented with fairness constraints, also asynchronous composition. Over structures without fairness constraints, the model-checking complexity of ATL is linear in the size of the game structure and length of the formula, and the symbolic model-checking algorithm for CTL extends with few modifications to ATL. Over structures with weak-fairness constraints, ATL model checking requires the solution of 1-pair Rabin games, and can be done in polynomial time. Over structures with strong-fairness constraints, ATL model checking requires the solution of games with Boolean combinations of Büchi conditions, and can be done in PSPACE. In the case of ATL, the model-checking problem is closely related to the synthesis problem for linear-time formulas, and requires doubly exponential time.
- 2003: In 2003 does Attie, P.C., Arora, A. and E.A. Emerson continue their work about mechanical synthesis of concurrent programs with the synthesis of fault-tolerant concurrent programs using CTL. In 2003 did Mäkelä M. publish his PhD thesis about EFFICIENT COMPUTER-AIDED VERIFICATION OF PARALLEL AND DISTRIBUTED SOFTWARE SYSTEMS. He provides a good overview of the subject. In the same year publish Popovic et al [231] a paper describing the combination of automated theorem proving with verification by applying reverse engineering of software into an adequat specification to be able to be used in theorem proving.
- 2005: In 2005 Kupferman and Vardi [179] relate linear time and branching time by the -calculus: Model checking is a method for the verification of systems with respect to their specifications. Symbolic model-checking, which enables the verification of large systems, proceeds by calculating fixed-point expressions over the system's set of states. The -calculus is a branching-time temporal logic with fixed-point operators. As such, it is a convenient logic for symbolic model-checking tools. In particular, the alternation-free fragment of -calculus has a restricted syntax, making the symbolic evaluation of its formulas computationally easy. Formally, it takes time that is linear in the size of the system. On the other hand, specifiers find the -calculus inconvenient. In addition, specifiers often prefer to use linear-time formalisms. Such formalisms, however, cannot in general be translated to the alternation-free -calculus, and their symbolic evaluation involves nesting of fixed-points, resulting in time complexity that is quadratic in the size of the system. In this article, we characterize linear-time properties that can be specified in the alternation-free -calculus. We show that a linear-time property can be specified in the alternation-free -calculus iff it can be recognized by a deterministic Büchi automaton. We study the problem of deciding whether a linear-time property, specified by either an automaton or an LTL formula, can be translated to an alternation-free -calculus formula, and describe the translation, when possible.
Another aspect is investigated by Puccella [237]: ``At the last TACAS in Barcelona, already almost a year ago, Alur, Etessami, and Madhusudan [2004] introduced CaRet, a temporal logic framework for reasoning about programs with nested procedure calls and returns. The details of the logic were themselves interesting (I will return to them later), but a thought struck me during the presentation, whether an axiomatization might help understand the new temporal operators present in CaRet. Thinking a bit more about this question quickly led to further questions about the notion of finiteness and infinity in temporal logic as it is used in Computer Science. This examination of the properties of temporal logic operators under finite and infinite interpretations is the topic that I would like to discuss here. I will relate the discussion back to CaRet towards the end of the article, and derive a sound and complete axiomatization for an important fragment of the logic.''
Machi, Tomita, and Hosono show the relative completeness of a version of CTL over possibly infinite states: ``It is based on a fair discrete system, which is with strong and weak fairness. Validity of a CTL formula is reduced to the validity of an assertion by eliminating the temporal operators and path quantifiers inductively. The idea is to represent the predicate describing that "a fair path begins with the current state" in the underlying assertion language using fixpoint operators.''
- In 2006 Beckert [32] gives an overview of the field of formal methods in software engineering for intelligent systems.
- 2007 In 2007 Das et. al. [73] investigate functional verification of task partitioning for embedded systems. They write: ``With the advent of multiprocessor embedded platforms, application partitioning and mapping have gained primacy as a design step. The output of this design step is a multithreaded partitioned application where each thread is mapped to a processing element (processor or ASIC) in the multiprocessor platform. This partitioned application must be verified to be consistent with the native unpartitioned application. This verification task is called application (or task) partitioning verification. This work proposes a code-block-level containment-checking-based methodology for application partitioning verification. We use a UML-based code-block-level modeling language which is rich enough to model most designs. We formulate the application partitioning verification problem as a special case of the containment checking problem, which we call the complete containment checking problem. We propose a state space reduction technique specific to the containment checking, reachability analysis, and deadlock detection problems. We propose novel data structures and token propagation methodologies which enhance the efficiency of containment checking. We present an efficient containment checking algorithm for the application partitioning verification problem. We develop a containment checking tool called TraceMatch and present experimental results. We present a comparison of the state space reduction achieved by TraceMatch with that achieved by formal analysis and verification tools like Spin, PEP, PROD, and LoLA.'' A different topic has been addressed by Vigano and Combetti [277] by applying symbol model checking to institutions: ``Norms defined by institutions and enforced by organizations have been put forward as a mechanism to increase the efficiency and reliability of electronic transactions carried out by agents in open systems. Despite several approaches have been proposed to model protocols in terms of institutional concepts (e.g., obligations and powers) and to monitor the actual compliance of agents' behavior at runtime, little work has been done to formally guarantee that such systems of norms ensure certain desirable properties. In this paper we describe a framework to verify institutions, which is characterized by a metamodel of institutional reality, languages to describe institutions and to specify their properties, and a tool to model check them. Finally, to evaluate our approach, we model and verify the Dutch Auction institution, a widely used interaction protocol, showing that the verification of institutional rules constitutes a necessary step to define sound institutions.''
- In 2008 there is another survey about automated techniques for formal software verification by D'Silva et al. [87]. A very extensive textbook has been published by Baier, C.; Katoen, J-P. [28]. This book is very clear, very exhaustive and here eventually preferable compared to the very good book of Berard et al (2001). But it is missing the overview about software tools which is very helpful in Berard et al.
- In 2009 Kröning et. [175] show with concrete examples, how one can apply model-checking to verify C-programs. But they show also the still given limits. Clarke, E. M. , Jr.; Emerson, E.A.; Siflakis, J. the founders of model checking, [60] present an overview of the actual situation of model checking in the year 2009.
Gerd Doeben-Henisch
2010-03-03