Capturing System Designs with Formal Executable Specifications

In my own experience, for a computational logic \(\mathcal {L}\) to be an expressive semantic framework for executable formal system design it is highly desirable that \(\mathcal {L}\) supports features such as the following:

Let me unpack requirement (6). By requirement (3), a theory T in \(\mathcal {L}\) specifying a given system defines a mathematical model of such a system as an initial model \(\mathcal {I}_{T}\), which is precisely the link between the system specification T and its formal requirements R. Formal requirements in R may be expressed in a variety of (typically non-computational) property specification logics. That is, each formal requirement \(\varphi \in R\) is a formula in one such logic. The link between T and R is then simple: T meets a formal requirement \(\varphi \in R\) iff \(\mathcal {I}_{T} \models _{\mathcal {L}'} \varphi \), where \(\mathcal {L}'\) is the property specification logic of formula \(\varphi \), and \(\models _{\mathcal {L}'}\) denotes the satisfaction relation between models and formulas in \(\mathcal {L}'\). For example, \(\mathcal {I}_{T}\) may provide the mathematical model of a communication protocol, and \(\varphi \) may express a safety or liveness property about such a protocol in some temporal logic. What (6) expects is that advanced algorithmic and deductive formal methods and tools are available to prove formal requirements about \(\mathcal {I}_{T}\) in various property specification logics \(\mathcal {L}'\), including logics expressing quantitative properties.

Maude’s [28] computational logic, namely, rewriting logic [24, 73] and its real-time and probabilistic extensions (see [63, 91]) provides a semantic framework for system specification meeting requirements (1)–(6). For how requirements (1)–(5) are met by rewriting logic and Maude see [30, 63, 71, 74, 75, 91]. I discuss in detail how Maude meets requirement (6) in §4.

I explain in §3 below how a computational logic \(\mathcal {L}\) meeting requirements (1)–(6) can support modular and reusable development of system designs by means of formal patterns.

Mathematically, a formal pattern is a theory transformation P that maps a declarative program in a computational logic \(\mathcal {L}\), that is, a theory T in the class \(\mathcal {C}\) of \(\mathcal {L}\)-theories satisfying the pattern’s input requirements, perhaps with some additional parameters \(\boldsymbol{p}\), into a new theory \(P(T, \boldsymbol{p})\) specifying the new correct-by-construction system generated by P, i.e., we can describe P as a (possibly partial) function,where \( Th _{\mathcal {L}}\) denotes the category of finitary theories in the language’s computational logic \(\mathcal {L}\). I assume throughout that \(\mathcal {L}\) enjoys the requirements presented in §2.1. We can therefore view P as a meta-program, that is, as a program that transforms a declarative program T into another declarative program \(P(T, \boldsymbol{p})\). Thanks to requirement (4) in §2.1 (logical reflection), programs in \(\mathcal {L}\) can be meta-represented as data structures,³ so that the meta-program P is also a program in the same computational logic \(\mathcal {L}\).

Although in some applications (e.g., [2]) the purpose of a formal pattern P may be one of optimization and/or specialization of a declarative program \(T \in \mathcal {C}\), in \(\mathcal {L}\), in many other applications \(P(T, \boldsymbol{p})\) may instead be a substantial extension of T with completely new features and capabilities; that is, \(P(T, \boldsymbol{p})\) is often a more sophisticated system, enjoying new features and properties not available in T. Nevertheless, the assume-guarantee properties of P often include the fact that P will in some appropriate sense be semantics-preserving. But in general this should not be understood in the sense that T and \(P(T, \boldsymbol{p})\) have the same semantics. Instead, the semantics of \(P(T, \boldsymbol{p})\) will often extend that of T while respecting T itself, which may remain intact as a subcomponent of \(P(T, \boldsymbol{p})\). This is in fact the case for many formal patterns (see, e.g., [4, 26, 39, 50, 110‐112]). From the point of view of code reusability this means that the code of T is not changed at all by P. That is, T is kept intact and encapsulated as a subcomponent. This gives formal patterns powerful modularity, code understandability and reusability, and verification scalability properties.

In yet other kinds of examples of formal pattern (e.g., [10, 63, 66, 68, 81]), the input theory T may not be kept as a subcomponent of \(P(T, \boldsymbol{p})\). Instead, the assume-guarantee properties relating T and \(P(T, \boldsymbol{p})\) may include considerably more general semantics-preserving properties such as the existence of a simulation or bisimulation (including the case of a stuttering simulation or bisimulation), between \(P(T, \boldsymbol{p})\) and T.

Formal patterns specified as Maude meta-programs have been defined and proved correct in various application areas, including:

Detailed discussion of the above formal patterns is beyond the scope of this paper. I refer to [76, 78] for overviews of many of them, and to the references given for each formal pattern for full details. Nevertheless, the P, \( Sim \), M and D transformations, as well as PALS, will make cameo appearances later in the paper.

After a talk by Shuo Chen at the University of Illinois reporting on how Maude had been used to uncover 13 types of previously unknown visual spoofing attacks on IE, my colleague Sam King came to my office and posed to me the following question, with roughly the following words:

Why don’t we design and build a browser that is secure by design?

Sam’s question exemplified the enormous advantage of ab origine uses of formal executable specifications over post facto uses: In a large system like IE with over one million lines of code, it was possible and very useful to use Maude to uncover and correct⁴ some security vulnerabilities; but it was essentially hopeless to achieve strong security guarantees about the IE implementation itself.

That conversation in my office was the start of a very fruitful 4-person (S. King, J. Meseguer, S. Tang and R. Sasse) collaboration on the design of such a secure-by-design browser: the Illinois Browser and Operating System (IBOS). Sam was the Ph.D. advisor of Shuo Tang, and I advised the Ph.D. of Ralf Sasse. Ralf was of course thoroughly familiar with Maude and formal verification. Shuo took my CS 476 course to also become familiar with specification and verification in Maude. The design of IBOS was captured in Maude from the very beginning of the project. Sam and Shuo took the lead on deciding the architecture of IBOS, including that of its small kernel, so as to meet specific security requirements, and also on implementing IBOS in C++, whereas Ralf and I focused on improving the Maude formal design and verifying its security properties. Shuo and Ralf interacted very closely, particularly to ensure that the C++ kernel implementation (about 60,000 lines of C++) developed by Shuo as part of his Ph.D. thesis [113] fully agreed with the Maude design. Ralf undertook the model checking verification of IBOS’s security properties as part of his Ph.D. thesis [100]. The four of us reported on the IBOS project and its formal specification and verification in [101]. A deductive verification of the IBOS security properties in reachability logic was later carried out in [106]. I summarize below the description of IBOS given in [101] and [106] and refer to [100, 101, 106, 107, 113] for further details.

The IBOS architecture can be graphically described as follows:

A key security property enforced by IBOS is the same-origin policy (SOP): it isolates web apps from different origins, where an origin is represented as a tuple of a protocol, a domain name, and a port number. The main components of IBOS are:

The security properties of IBOS can be formally expressed as an invariant P, which is itself a conjunction \(P = \bigwedge _{1 \le i \le 11} P_{i}\) of eleven simpler invariants [106]. P implies the two main security properties of IBOS, namely, (i) SOP, which is the conjunction \( SOP =\bigwedge _{1 \le i \le 11} P_{i}\), and (ii) the address bar correctness (ABC) property, which is \(P_{10}\). The invariant \(\bigwedge _{1 \le i \le 10} P_{i}\) was verified by Ralf Sasse by model checking [100, 101], whereas P itself was deductively verified in reachability logic by Stephen Skeirik as part of his Ph.D. thesis at Illinois [106, 107].

The formal design, verification and implementation in Maude of the Read atOmicity and prevention of Lost updAtes (ROLA) distributed database [65] is part of a much bigger joint effort by researchers at the University of Illinois and the University of Oslo to formally specify in Maude and to verify the qualitative (consistency properties) and quantitative (performance properties) of a wide range of industrial and academic distributed databases. To the best of my knowledge, this was the first time that those distributed databases, lacking in virtually all cases any prior formal specifications, were thus formally specified in Maude and analyzed with respect to their consistency and performance properties. I refer to the survey [17] for details about this bigger research effort. What is unique about both ROLA, as compared to all the other industrial and academic distributed data bases described in [17], is that the Maude specifications of all other databases were post facto efforts to specify and verify systems already implemented.⁵ Instead, ROLA was designed, verified and implemented in Maude ab origine.

Another unique aspect of ROLA is that it illustrates how easy, fast and inexpensive it is to explore the design space in search of an optimal design (w.r.t. given requirements) by means of executable formal specifications. As already pointed out in §1, it is usually very costly, and seldom done, to explore design alternatives for a system developed from informal specifications. But it is even more difficult and costly to compare different distributed systems with respect to some correctness and performance requirements. To begin with, different systems may be implemented in different programming languages, so that experimentally comparing their behavior and performance may not allow answering the counterfactual question: How would they compare if they had been implemented in the same programming language? Answering this question might provide partial evidence for the really crucial question: Is the design of system A better than that of system B w.r.t. some given correctness and performance requirements? Let me explain how the design of ROLA provides an answer to this question.

Most modern distributed databases have large numbers of users, sometimes located all over the world, with data stored and replicated across various data centers. For these systems performance, and specifically availability, is as important as correctness, and specifically database consistency properties. In distributed database design there is an unavoidable tension between consistency and availability, particularly when the network can be partitioned [23]. The fine art of distributed database system design involves finding the right balance between availability and consistency in the design space. Such a balance actually depends on the kinds of applications envisioned for the given database. For example, the database of a social network will typically have considerably weaker consistency requirements than those of a bank or a medical information system; and this can be exploited to increase the performance of a social network.

Exploring the distributed database design space can be guided by the degree of database consistency needed for the system in question. Providing a greater degree of consistency than necessary for a given application will often result in loss of performance, including poorer availability. The work of Cerone et al. [25] has provided a formal axiomatization of a hierarchy of increasingly stronger consistency models —with read atomicity (RA) as the weakest and serializability (SER) as the stronger—, as pictured in the black-marked models of the consistency hierarchy of Figure 1 from [65]. The significance of ROLA is that it found a previously unexplored sweetspot in the design space by adding one more node to the consistency hierarchy of [25], namely the update atomic (UA) consistency, marked in red in Figure 1, and has demonstrated clear performance advantages for this sweetspot, which is well suited for social media applications. The potential usefulness of UA was already conjectured in [25], but was left as a future possibility.

Due to space limitations I refer to [25] for further details on the consistency models in Figure 1, and to [65] for a more detailed discussion of other related consistency models and properties. For my design exploration purposes here, the question I would like to focus on is: What database system designs ensuring either parallel snapshot isolation (PSI) (the node right below UA) or something slightly weaker than PSI existed prior to ROLA? The answer is that two such system designs existed, namely, the Walter protocol [108] implementing PSI, and the Jessy protocol [6], implementing the non-monotonic snapshot isolation (NMSI) consistency model, which is weaker than PSI but satisfies causal consistency (CC). Note that, unlike Walter and Jessy, ROLA does not satisfy CC, but, as explained in [65], CC is not essential for social network applications such as friendship networks. The main question then is: What are the gains in performance obtained by focusing on the UA sweetspot? As I pointed out above, this question would be hard to settle by comparing system implementations of Walter, Jessy and ROLA. Furthermore, it would require implementing ROLA before any such comparison became possible, thus defeating the design exploration purpose. However, based on Maude formal executable specifications of Walter, Jessy and ROLA (with the replication features of Walter and Jessy disabled to obtain a fair comparison), and enriching these three specifications with a common probability distribution on the time required for inter-node communication to obtain three associated probabilistic rewrite theories [63], it has been possible to answer this question by statistical model checking analysis using the PVeStA tool [3]. The answer is that, as shown in Figure 2 from [65], ROLA clearly outperforms both Walter and Jessy in all performance requirements for all read/write transaction rates.

For the model checking verification of ROLA’s consistency requirements I refer the reader to §6 of [65]. This still leaves open the matter of ROLA’s implementation, and raises the question of how consistent would the ROLA performance predictions be with experimental evaluations of ROLA. These two issues were addressed in the subsequent paper [68]. In fact, [68] answered a much broader question, namely:

Is it possible to automatically generate a correct-by-construction implementation of a distributed system design priorly captured in Maude?

This question was answered by means of a formal pattern, namely, the D-transformation mentioned in §3.2. The point is that Maude is not only a language to model and verify properties of concurrent systems using the Maude interpreter and its formal tools. Thanks to its support for external objects, including TCP/IP sockets, it is also a language to program and implement open distributed systems [33]. What the D-transformation formal pattern does is to transform an object-oriented system design in Maude into a distributed implementation of it, also in Maude, that is stuttering bisimilar to the design. Using the D-transformation it was then possible to automatically transform the ROLA Maude design into a ROLA implementation and to experimentally evaluate ROLA. As explained in [68], ROLA’s distributed implementation was experimentally evaluated in two different scenarios, named ROLA\(\_\)A and ROLA\(\_\)B, and the performance predictions for each scenario obtained by statistical model checking of the ROLA design were compared with the corresponding experimental evaluations of its implementation. These results are summarized in Figure 3 from [68] and show a substantial agreement between the ROLA performance predictions and the corresponding experimental evaluations. I refer to [68] for further details.

Ptolemy II [41] is a widely used graphical modeling and simulation language tool for real-time and embedded systems. It supports design and simulation of concurrent, real-time, embedded systems expressed in several models of computation (MoCs), such as state machines, data flow, and discrete-event models, that govern the interaction between concurrent components. A user can visually design and simulate hierarchical models, which may combine different MoCs. Furthermore, Ptolemy II has code generation capabilities to translate models into other modeling or programming languages such as C or Java. Discrete-Event (DE) models are among the most central in Ptolemy II. Their semantics is defined by the tagged signal model [56]. The work by Bae et al. in [11, 14] endows DE models in Ptolemy II with formal analysis capabilities by: (i) defining a semantics for them as real-time rewrite theories; (ii) automating such a formal semantics as a model transformation using Ptolemy II’s code generation features; (iii) providing a Real-Time Maude plugin, so that Ptolemy II users can use an extended GUI to define temporal logic properties of their models in an intutitive syntax and can invoke Real-Time Maude from the GUI to model check their models. Let us see an example.

A Ptolemy Example. Figure 4 shows a Ptolemy II model from [14] of a fault-tolerant traffic light system at a pedestrian crossing, consisting of one car light and one pedestrian light. Each light is represented by a set of set variable actors (Pred and Pgrn represent the pedestrian light, and Cred, Cyel, and Cgrn represent the car light). A light is on iff the corresponding variable has the value 1. The Finite State Machine (FSM) actor Decision “generates” failures and repairs by alternating between staying in location Normal for 15 time units and staying in location for Abnormal for 5 time units, and by sending events to the TrafficLight through its Error and Ok ports accordingly. During normal operations, the lights are controlled by the FSM actors CarLight and PedestrianLight (their FSM’s are not shown in the figure) that send values to set the variables; in addition, CarLight sends signals to the PedestrianLight actor through its Pgo and Pstop output ports.

For M this hierarchical Ptolemy II model, the semantic mapping \(M \mapsto \llbracket M \rrbracket \) realized as a Real-Time Maude plugin associates to M a Real-Time Maude specification that can then be formally analyzed by model checking. I refer to [14] for further details about the real-time rewrite theory \(\llbracket M \rrbracket \) for this example and the formal verification of its properties.

Real-Time Maude analysis (including automatically generating Real-Time Mude models from Ptolemy II models) of such Ptolemy II DE models has been integrated into Ptolemy II, and has been used, e.g., to uncover a previously undetected flaw in the raffic light model: The yellow light may not be blinking when the taffic light system is in Abnormal mode [60].

AADL (http://​www.​aadl.​info/​) is a standard for modeling embedded systems that is widely used in avionics and other safety-critical applications. However, AADL lacks a formal semantics, which severely limits both unambiguous communication among model developers and the formal analysis of AADL models. In [94] Ölveczky et al. defined a formal object-based real-time concurrent semantics for a behavioral subset of AADL in rewriting logic, which includes the essential aspects of AADL’s behavior annex. Such a semantics is directly executable in Real-Time Maude and provides an AADL simulator and LTL model checking tool called AADL2Maude. AADL2Maude is integrated with OSATE, so that OSATE’s code generation facility is used to automatically transform AADL models into their corresponding Real-Time Maude specifications. Such transformed models can then be executed and model checked by Real-Time Maude. One difficulty with AADL models is that, by being made up of various hierarchical components that communicate asynchronously with each other, their model checking formal analysis can easily experience a combinatorial explosion. However, many such models express designs of distributed embedded systems which, while being asynchronous, should behave in a virtually synchronous way. This suggests the possibility of using the PALS formal pattern [80] already mentioned in §3.2, which reduces distributed real-time systems with virtual synchrony to synchronous ones, to pass from simple synchronous systems, which have much smaller state spaces and are much easier to model check, to semantically equivalent asynchronous systems, which often cannot be directly model checked but can be verified indirectly through their synchronous counterparts. This has led to the design of the Synchronous AADL sublanguage in [13], where the user can specify synchronous AADL models by using a sublanguage of AADL with some special keywords. A synchronous rewriting semantics for such models has also been defined in [13]. Using OSATE’s code generation facility, synchronous AADL models can be transformed into their corresponding Real-Time Maude specifications in the SynchAADL2Maude tool, which is provided as a plugin to OSATE. Likewise, the user can define temporal logic properties of synchronous AADL models based on their features, without requiring knowledge of the underlying formalism, and can model check such models in Real-Time Maude. More recently, Bae and others have extended Synchronous AADL, including the integration into OSATE, to multirate systems [16], hybrid systems [57, 59], and multirate hybrid systems [12, 58]. In the hybrid systems cases, the semantics is formalized using rewriting modulo SMT, and the main forms of analysis supported are randomized simulation, (bounded) symbolic reachability analysis, and their combination. Somewhat surprisingly, the performance of such Maude-with-SMT reachability analysis in many cases outperforms dedicated hybrid automata reachability tools such as HyComp, SpaceEx, Flow\(*\), and dReach [59]. The effectiveness of HybridSynchAADL and MR-HybridSynchAADL has been illustrated on systems of collaborating drones.

A Synchronous AADL Example (from [13]). I sketch below a model of an avionics system based on a specification by Steve Miller and Darren Cofer at Rockwell-Collins [83]. A full description of this model is given in [13]; here I just give an impressionistic description of it and refer to [13] for additional details. The details, as such, are not the point of the example: the key point is to illustrate the idea that a synchronous AADL model can be viewed as a synchronous composition of state machines (one such machine per AADL component), which are formalized in the Real-Time Maude semantics as separate objects that change their state synchronously.

In integrated modular avionics (IMA), a cabinet is a chassis with a power supply, internal bus, and general purpose computing, I/O, and memory cards. Aircraft applications are implemented using the resources in the cabinets. There are always two or more physically separated cabinets on the aircraft so that physical damage does not take out the computer system. The active standby system considers the case of two cabinets and focuses on the logic for deciding which side is active. Each side can fail, and a failed side can recover after failure. In case one side fails, the non-failed side should be the active side. In addition, the pilot can toggle the active status of the sides. The full functionality of each side depends on the two sides’ perception of the availability of other system components. An AADL-like graphical description of the system is shown in Figure 5, and the following is a fragment of its top-level textual representation, which declares the architecture of the system, with the three subcomponents sideOne, sideTwo, and env, and with immediate data connections (denoted by the arrow ‘-​>​’) from the environment to the two sides, and with delayed data connections (‘-​>​>​’) between the two sides. Each subcomponent contains a thread specification (not shown) in AADL’s behavior annex.

Again, as for Ptolemy II, the key point for AADL is that, for M a synchronous AADL model, the semantic mapping \(M \mapsto \llbracket M \rrbracket \) realized as an AADL plugin associates to M a Real-Time Maude specification that can then be formally analyzed by model checking. For the details of how this is done for the above active standby example I refer the reader to [13]; and for examples in the further extended plugins of Synchronous AADL to [12, 16, 57‐59].