Prospec

Prospec: Support for Elicitation and Formal Specification of Software Properties Oscar Mondragon, Ann Q. Gates, and Steven Roach The University of Texas at El Paso Department of Computer Science oscar, agates, [email protected] Abstract Although formal verification techniques have been demonstrated to improve program dependability, software practitioners have not widely adopted them. One reason often cited is the difficulty in writing formal specifications. This paper introduces Prospec, a tool to assist practitioners in formally specifying software properties. Prospec uses property patterns and scopes. Previous efforts at providing tool support for property specification have not provided convenient abstractions for specifying properties that include multiple events or conditions. A taxonomy of composite propositions is introduced to address this issue by defining relations among propositions and providing graphical abstractions that can assist in specification and validation of properties. This paper shows how composite propositions can enhance the specification pattern system by helping practitioners consider subtleties of behavior in sequences and concurrency through directed questions and visual abstractions. The paper introduces an elicitation and specification process to define patterns, scopes, and composite propositions.

1. Introduction Runtime monitoring techniques have been successful at identifying subtle software errors missed by testing [2]. To be effective, monitoring requires the elicitation and specification of software properties that define correct program behavior; however, specifying properties formally and accurately is difficult. The following reasons have been cited: ƒ the high level of mathematical sophistication and training required to specify properties[5]; ƒ lack of common software development packages that provide tool support for formal specification[8]; and ƒ difficulty of reading and understanding specifications [4, 22], making them challenging to validate. This paper introduces a tool called Property Specification (Prospec) that provides visual and textual guidance for specifying common properties of systems. Prospec provides a process for elicitation and specification of properties and generates formal specifications in Future Interval Logic (FIL), Linear Temporal Logic (LTL), and the Meta Event Definition Language (MEDL) that can be used by a variety tools such as theorem provers, model checkers, and runtime monitors. In addition, it helps reduce errors in formal specifications by facilitating the definition of sequential and concurrent behavior, identification of patterns and scopes, and validation of specifications. This work builds on the Specification Pattern System (SPS) [5, 6]. It addresses SPS’s limitations by supporting the specification of concurrent behavior and extending the type of sequences that can be applied to specification patterns. 1

The paper is organized as follows. Section 2 provides brief descriptions of software properties, SPS, and FIL. Section 3 describes properties of the Bay Area Rapid Transit system. One property is used as an example throughout the paper. Section 4 describes Prospec and how the tool guides the user in selecting patterns, scope, and composite propositions. It also describes how visual abstractions enhance the description of the properties expressed by the response pattern. The visual abstractions highlight subtle differences in the structure of sequential and concurrent behavior. Section 5 describes the generation of MEDL formulas for use by the Monitoring and Checking system for runtime monitoring. Section 6 discusses related work. The paper ends with a summary and future work.

2. Background This section introduces property specifications and SPS. It also provides an introduction to FIL, which is one of the formal specification languages generated by the tool. 2.1. Property Specification A software property is a description of desired software behavior, e.g., the value of variable balance must always be non-negative. Properties can be asserted to hold over the entire system execution or over a bounded interval of program execution, and they can be expressed as conditions or events. A condition denotes a proposition that holds in one or more consecutive states. An event denotes an instant of time at which a condition changes value. While conditions are used to describe concurrency, events can describe activation or synchronization of processes or actions. Numerous formalisms for expressing properties exist, including algebra-based, model-oriented, automata-based, functional, logic-based, and natural languages. Regardless of the language chosen to express properties, the properties must be written in a language understandable by the domain experts for validation purposes and understandable by verification techniques in order to be useful. A survey of run-time monitors [2] summarizes a variety of approaches for specifying properties. Temporal Logic (TL) [16] has been used over the last two decades to express properties about program behavior, especially reactive and concurrent systems. Specifying intervals in a linear temporal logic is difficult because the only relevant construct is the until temporal operator. Extensions to TL such as Interval TL (ITL) [18] facilitate the specification of the scope over which a property must hold. ITL is a linear temporal logic that provides special constructs to handle intervals that can be used to specify the scope over which a property is asserted. Classifying properties is one approach for helping practitioners identify and specify common types of behaviors. Lamport [13] described the safety-liveness classification identifying two disjoint categories of system properties: safety (something bad never happens) and liveness (something good eventually happens). Subsequently, Manna and Pnueli [16] defined a more detailed classification for system properties based on Boolean combinations of formulas of the form □p and □◊q. The identified classes of properties are safety, termination, recurrence, and persistence. Safety occurs at all states of the sequence; 2

termination occurs at some states of the sequence; recurrence occurs at infinitely many states of the sequence; and persistence occurs at all but finitely many states of the sequence. 2.2. Specification Pattern System SPS [5] provides patterns and scopes to assist practitioners in the formal specification of a property in languages such as LTL [1], CTL [14], and GIL [3]. Patterns are high-level abstractions that provide descriptions of a “commonly occurring requirement on the permissible event or state sequence in a finite state model of a system” [5, p. 412]. Through a website, SPS presents pattern taxonomy. A pattern contains intent, motivation, and known uses [7]. Each pattern is associated with a scope that defines the sequence of states over which a property holds during program execution. After selecting a pattern and a formal specification language, the mapping for each scope in the selected language is presented. The main SPS patterns are universality, absence, existence, precedence, response, chain precedence, and chain response. Universality properties are true in every point of the execution; absence properties are never true during the execution; existence properties are true at some point in the execution; precedence properties require that a given state or event always occurs before a designated state or event occurs; and response properties require that the occurrence of a given state or event be followed by a designated state or event. Response properties represent a temporal relation called cause-effect between two propositions. A cause-effect relation states that if proposition p1 is asserted, then some time in the future proposition p2 must also be asserted. The chain pattern handles multiple sequence of states. Chain precedence and chain response specify properties on sequences of states or events and are generalizations of precedence and response, respectively. 2.3. Future Interval Logic Future Interval Logic (FIL) [19] is a language based on the interval temporal logic by Schwartz et al. [20]. FIL is used to specify the behavior and properties of reactive systems. FIL manages the scope of reasoning through intervals of time and facilitates compositional and hierarchical reasoning. A specification in FIL consists of formulas and intervals. A formula describes a property of the system, while an interval defines the states of interest. A computation is a sequence of states, σ = s0, s1, s2,…, with a discrete linear order. An interval is a subsequence of a computation. A pair of search patterns defines the boundaries of an interval. A search to a formula g, depicted as →g, identifies the first state in an interval at which g holds. A search to formula g fails if g does not hold at any state in the interval. A search to g succeeds at its starting state if g holds in this state. Informally, a search pattern is a sequence of searches. Searches in a sequence start where the previous search ended (except for the first search, which starts at the beginning of the interval). Let g, h, and i be formulas and →g, →h, →i denote a search pattern. if g, h, and i hold at the same state then the search pattern is asserted in one state.

3

An interval formula contains a pair of search patterns, called the left and right search patterns. If α and β are search patterns, then [α | β) p is an interval formula, where formula p is asserted at the first state of interval [α | β). Intervals are half-open on the right so that the interval includes the state found by α and subsequent states up to but not including the state found by β. The interval is built when both search patterns succeed and the state found by the left search α precedes the state found by the right search β. If the interval [α | β) cannot be built, then [α | β) p vacuously holds. There are two special cases of intervals. A prefix interval, denoted [– | β), begins at the start of its parent interval. A suffix interval, denoted [α | →), terminates at the end of its parent interval. In both cases, if no parent interval is specified, the entire computation is used. A search to the end of an interval, denoted →, always succeeds. FIL formulas are defined recursively [10] as follows. ƒ Propositions and the constants true and false are formulas. ƒ If F is a formula, then ¬ F, ◊F, and □F are formulas. ƒ If F1 and F2 are formulas, then F1 ∨ F2, F1 ∧ F2 , and F1 ⇒ F2 are formulas. If α and β are search patterns and F is a formula, then [α | β)F, [ - | β)F, and [α | →)F are formulas. A search pattern is either “→F” or a sequence of searches written “→F, α”, where α is a search pattern. For example, [α | β) [χ | δ) p is interpreted by finding the interval defined by search patterns α and β. The search χ begins at the state identified by α. The search δ must succeed at or before the state identified by β. Formula p holds at the first point of interval [χ | δ). The eventual (◊) and henceforth (□) operators are defined in FIL [10] as follows: ◊F ≝ ¬ [→F | →) false; □F ≝ ¬◊ ¬ F. This definition for ◊F is not obvious. Recall that if a search to F fails, the formula [→F | →) false vacuously holds; thus, the negation (¬) makes the formula false. If a search to F succeeds, false is asserted, and then the negation (¬) makes the formula true. That is, the eventual formula ◊F asserts that, if a search to F fails, the formula returns false, and if a search to F succeeds, then the formula returns true. A strong search to formula F, denoted → * F, asserts that the search to F must succeed, i.e., a state where formula F holds must be located. The strong search is defined [10] as follows: [α, → * F1 | β) F2 = [α, → F1 | β) F2 ∧ [α | →) ◊ F1 [α | β, → * F1) F2 = [α | β, → * F1) F2 ∧ ( [α | →) false ∨ [β | →)◊ F1) In other words, the strong search to formula F1 requires that F1 eventually holds. If F1 does not hold, then the interval formula evaluates to false. The semantics of FIL can be found in [10]. FIL does not support the next temporal operator, and its interpretation of future includes the present. ƒ

3. Examples from BART Case Study To motivate the need for automated support in elicitation and specification of properties, two properties from the Bay Area Rapid Transit District Advance 4

Automated Train (BART) train control system [23] are presented. The BART system controls rapid transit in the San Francisco Bay area. Trains have an onboard computer system and regions are controlled by a centralized command system. Speed and acceleration commands are sent by the central system to each train every half second. These commands are issued based on data received from the system. Commands are time stamped and become invalid two seconds after the identified time. In this case, worse case is assumed and the train stops. FIL is used to specify the properties. The reader should note that, although the example properties are straight forward, the FIL specifications are non-trivial. The specifications are revisited after Prospec is described to illustrate how the tool supports the specification. 3.1. BART Property P1 Property P1 states: If wheel slippage is detected when the maximum brake rate is being applied, the breaking force is reduced so that wheel adhesion can be regained. The following propositions are defined: ƒ WS – Wheel slippage is detected. ƒ MB – Maximum braking force is being applied. ƒ RB – Breaking force is reduced. ƒ ¬WS – Wheel adhesion is regained. The FIL specification is as follows: □ ( ([→(WS ∧ MB) | →*¬WS) □ RB) ∨ ([→(WS ∧ MB) | →) □ (RB ∧ WS)) ) The formula asserts that the disjunction of the two sub-formulas holds throughout the computation. The first sub-formula states that RB holds throughout the interval, which starts at the first state in which WS and MB hold and ends in a future state when ¬WS holds. The second sub-formula states that RB and WS hold throughout the interval that starts at the first state in which WS and MB hold and terminates at the end of the computation. 3.2. BART Property P2 Property P2 states: If a command expires, the train applies maximum braking until either the train stops or a new command is received. The following propositions are defined: ƒ CE – The command is expired ƒ MB – Maximum braking force is being applied. ƒ ST – The train is stopped. ƒ NC – New command is received The FIL specification is as follows: □ ( [→CE | →(ST ∨ NC) ) □ MB) The formula states that MB is true during all intervals that start when CE is true and end when either ST or NC is true.

4. Prospec Although SPS patterns are parameterized, adapting the resulting specification to complex properties requires expertise in the area of formal methods. For a 5

general practitioner, refinement of the specification can be difficult. SPS does not provide convenient abstractions for specifying concurrent behavior such as synchronization and non-determinism. Furthermore, the only sequences considered in SPS are those that occur in non-consecutive states, i.e., those in which one event follows another without constraining the number of states between each event. Patterns also do not provide convenient abstractions for defining relations involving multiple propositions, e.g., relations used to define concurrent behavior such as synchronization and non-determinism. The goal of Prospec is to enhance SPS by supporting the specification of concurrent system behavior and extending the type of sequences that can be applied to specification patterns. Prospec automates the elicitation process and guides the practitioner in the determination of patterns, scopes, and relationships among propositions. The tool automates the generation of a formal specification that can be used by a variety tools, in particular, runtime monitors. Prospec helps the practitioner consider aspects of a property that may not have been considered, and it highlights the subtleties associated with related SPS patterns and scopes. In Prospec, elicitation is part of the specification process. Guided questions force the user to consider aspects of the problem that may not have been considered previously. This may cause him or her to enhance the original specification, validate the enhancements, and record any assumptions that are made. In the remainder of the paper, the term “specification process” implies that this form of elicitation is part of the process. This section describes Prospec by reviewing the interfaces of the tool. Prospec specifications are comprised of scopes and patterns that are enhanced with composite propositions when multiple conditions or events are used. These interfaces are described first. Next, an interface called Commonly Specified Behavior is described. This interface provides specialized assistance for specifying response formulas. The last interface described is the main interface, which shows the generated specification. The BART examples from Section 3 are used to motivate the features of these interfaces. 4.1.1. Specifying Scope The scope indicates the extent of program execution, i.e., the interval, over which a property is considered. Conditions or events may define the left (L) and right (R) boundaries of the interval. Fig. 1 shows Prospec's Scope screen with SPS’s graphical representation of the five main scopes: global, before L, after L, between L and R, and after L until R. Global indicates that a pattern holds throughout the program execution; before L indicates that a pattern holds during program execution before L first occurs; after L indicates that a pattern holds during program execution after L first occurs; between L and R indicates that a pattern holds during execution between the first occurrence of L and the next occurrence of R; and after-until indicates that the property holds during execution between the first occurrence of L and until the next occurrence of R or the end of the program execution. Scopes are parameterized. For instance, global scope has no parameters; scopes before and after have one parameter; and scopes between and after-until have two parameters. 6

Figure 1: Property scope screen. Prospec allows experienced users to select a type of scope by clicking on an associated radio button as shown on the left side of Fig. 1. When a scope is selected, the window displays a description of that scope at the bottom of the screen. The description summarizes information that distinguishes one scope from others. For instance, the description for Before R scope provides the following information: the scope does not include R, the scope starts at the beginning of the execution, only the first occurrence of R is considered, and the scope is not repeated. Prospec can also provide assistance in specifying scope when the user clicks on Guided Selection. This displays a series of questions that lead to the selection of scope. Fig. 2 shows the questions in the form of decision tree. The right part of the screen in Fig. 1 is provided to gather the propositions that comprise the left and/or right boundaries of the scope. Based on the selected scope, the appropriate boundary is enabled. The propositions associated with a boundary are added, modified, and removed by the New, Edit, and Delete buttons, respectively. When a boundary is comprised of more than one proposition, the composite propositions frame is enabled, allowing the practitioner to define the behavior associated with these propositions. The Select CP button takes the user to the window shown in Fig. 5 to facilitate this. For BART property P1, the responses to the decision tree are as follows: 1. Is the interval of program execution over which the property is being considered repeatable? Yes. 7

2. Is the right boundary always required for each interval? No. Is the interval over which the property is being considered repeatable during program execution? yes

no

Is the right boundary always required for each interval? yes Between L and R

Is the left boundary defined by the beginning of the execution?

no

yes

After L Until R

Is the right boundary defined by the end of the execution? yes Global

no

After L

no Before R

Figure 2: Decision tree for identifying scope. This leads to the after L until R scope. In the Boundaries frame, L and R are enabled. Propositions WS (wheel slippage is detected) and MB (maximum braking force is being applied) define L. Proposition ¬WS (wheel adhesion is regained) defines R. The Select CP button is enabled for L. Defining the scope of a property may constrain the verification technique to be used. For instance, run-time monitors cannot identify violations to liveness properties, i.e., guarantee properties [16] or existence patterns with a global scope [5]. Run-time monitoring can assert universality and absence patterns in combination with any scope. A monitor can assert violations to existence patterns only if the end of the scope is finitely bounded. 4.2. Specifying Patterns In Prospec, the SPS patterns considered are: universality, absence, existence, precedence, and response. SPS chain patterns are not included. Instead, Prospec uses composite propositions (see Section 4.3) to capture sequential or concurrent behavioral structures in patterns or scope boundaries. This allows sequences to be used beyond response and precedence patterns. Fig. 3 shows Prospec's Pattern screen. The top left frame of the screen presents a list of SPS pattern names and associated state sequence diagrams. Prospec introduces the state sequence diagrams to assist users in both visualizing the behaviors associated with each pattern and understanding the difference between pattern behaviors. In these diagrams, the horizontal line shows time progressing from left to right. Circles denote states and the labels represent the propositions that are asserted at that state. Some patterns may have more than one diagram, where each represents a behavior associated to that pattern. The View All button next to the precedence and response patterns allows the user to view the various behaviors associated with these patterns. This information assists users to decide whether the pattern represents the intended behavior of the property being specified. Below the property pattern frame, a description for the selected pattern is provided. As with scope, the description presents information about the pattern that can be used to distinguish it from others. For instance, the description for the Precedence (T, P) pattern indicates that a cause T precedes each effect P; P does 8

not occur before T; P does not occur at the same state as T; and P may not occur even if T occurs.

Figure 3. Property specification pattern screen. Patterns have one or two parameters, denoted as T and P. The right frame in the screen of Fig. 3 is used to gather the propositions associated with these parameters. Based on the selected pattern, the appropriate parameter is enabled. The functionality for adding, modifying, and deleting propositions is the same as the one provided for the scope screen. If more than one proposition is added, the composite propositions class frame is enabled. For BART property P1, between detecting wheel slippage and wheel adhesion being regained, the braking force is continuously reduced. Thus, the pattern that applies is universality with proposition P defined as RB. 4.3. Specifying Composite Propositions Composite propositions (CP) identify relations among multiple propositions. Multiple propositions may be used to define boundaries of scopes and structure of behavior as provided by SPS patterns. For instance, an ordered sequence may define the left boundary of an after L scope and events that represent the synchronous start of multiple tasks may define the T parameter of a T response P pattern. Composite propositions may denote conditions and events. While conditions are used to describe concurrency, events describe activation or synchronization of processes or actions. The composite proposition taxonomy categorizes and defines the structure of multiple propositions. The CP taxonomy has twelve classes. Each class defines a 9

detail structure for either concurrent or sequential behavior. The leaves of the tree shown in Fig. 4 depict the six CP classes in which propositions are being considered as conditions. The other six CP classes are similar to those given in this figure, but the propositions are considered as events.

Hold - quantification AtLeastOne

All

Hold-time

AtLeastOneC

Different

Same

Elapse-time Eventual

Consecutive

Ordering

Ordering Deterministic ConsecutiveC

ParallelC

non-determ. ConsecutiveC*

Deterministic EventualC

non-determ. EventualC*

Figure 4: CP taxonomy based on conditions Table 1: Syntax and description of composite proposition classes. Informal description LTL Definitiion

Syntax

AtLeastOneC(G) AtLeastOneE(G) ParallelC(G) ParallelE(G)

ConsecutiveC [G] ConsecutiveE [G] EventualC[G]

EventualE[G]

At least one of the propositions in the set G holds. At least one of the propositions in the set G becomes true. All propositions in the set G hold. All propositions in the set G become true. Each proposition in the sequence G is asserted to hold in a specified order, one at each successive state. Each proposition in the sequence G becomes true in a specified order, one at each successive state. Once they become true, their true value does not matter. Each proposition in the sequence G is asserted to hold in a specified order and in distinct and possibly nonconsecutive states. Each proposition in the sequence G becomes true in a specified order and in distinct and possibly nonconsecutive states. Once they become true, their true value does not matter.

p1 ∨ p2 ∨ … ∨ pn (¬p1 ∧ ◊p1) ∨ (¬p2 ∧ ◊p2) ∨ … ∨ (¬pn ∧ ◊pn) p1 ∧ p2 ∧ … ∧ pn (¬p1 ∧ ¬p2 ∧ … ∧ ¬pn) ∧ ((¬p1 ∧ ¬p2 ∧ … ∧ ¬pn) U (p1 ∧ p2 ∧ … ∧ pn)) p1 ∧ o(p2 ∧ … ∧ o(pn) …) (¬p1∧¬p2∧… ∧¬pn) ∧ o((p1∧¬p2∧… ∧¬pn) ∧ o((p2∧¬p3∧… ∧¬pn) ∧… ∧ o(pn) …))

p1 ∧ o(◊(p2 ∧ … ∧ o(◊(pn)) …)) ¬p1 ∧ (¬p1 ∧ … ∧ ¬pn) U ((p1 ∧ ¬p2) ∧ (¬p2∧… ∧¬pn) U ((p2 ∧ ¬p3) ∧ (¬p3∧… ∧¬pn) … U ((pn-1 ∧ ¬pn) ∧ (◊pn) …)))

The taxonomy is given as a rooted binary tree where each node denotes a decision point and each edge represents a decision. Assume a node n is associated with a decision point P(d1,d2), then the label of the left child of n is associated with decision d1 and the right child of n is associated with decision d2. Each child of a decision point is named accordingly except in the case of a leaf node, which names a class of composite propositions. Each level, except the last, is named based on the decision point(s) applied at that level. A path from the root to a leaf node represents a series of decisions. The leaf nodes denote classes that define the structure of behavior associated with multiple propositions. 10

Table 1 gives the syntax, informal descriptions, and semantics specified in LTL for the CP classes. A CP class includes: a) the name of the class with a sub-index C or E to distinguish between propositions that are asserted as conditions and those asserted as events; and b) a parameter [G] or (G) that denotes a sequence of propositions, i.e., (p1, …, pn), or a set of propositions, i.e., {p1, …, pn}, respectively. Commas separate propositions in G. Note that a proposition p holds at state si if p is true at si. Also, a proposition p becomes true if p is false in some state and, at a future state, p is true. The term p becomes true is used to denote an event. Propositions that are asserted to hold in a CP class are regarded as conditions. The formal semantics for composite propositions are given in LTL [17]. As with patterns, two methods of selecting CP are available to the user. Users can select a CP class by selecting an appropriate radio button, or the user can use the Guided Selection option. The CP screen shown in Fig. 5 is enabled when multiple propositions are used to specify a pattern or scope. The screen displays each CP class for the type selected (see button that switches type from Condition to Event), including its name, graphical symbol, and timeline diagram. To assist the analyst in understanding, specifying, and validating composite propositions, a symbol and a timeline diagram are used as shown in Fig. 5. This provides an alternative to the set of guided questions. The symbol and timeline diagrams provide different perspectives and assist in identifying the intent of each class. When the user clicks on Guided Selection, a set of guided questions, which correspond to the tree given in Fig. 4, are displayed as follows: 1. Are the propositions being asserted as conditions or as events? CP classes have a C or E subscript when propositions are considered as conditions or events, respectively. 2. Do all propositions have to hold or does only one proposition have to hold? If only one proposition has to hold, then the selected CP class is AtLeastOne; otherwise, continue with the next question. 3. Are the propositions asserted at the same point in time or at different points in time during program execution? Note that this question addresses simultaneity of propositions. If propositions are asserted at the same point in time, then the selected CP class is Parallel; otherwise, continue with the next question. 4. Are the propositions asserted at consecutive or non-consecutive units of times? This answer along with the answer to the next question determines the rest of the class. 5. Are the propositions asserted in a predefined order or is the ordering of the propositions non-deterministic? If the answers are “in consecutive units of time” and “in a predefined order,” then the CP class is Consecutive. If the answers are “in consecutive units of time” and “in a non-deterministic order,” then the CP class is Consecutive*. When propositions hold in nonconsecutive units of time, the CP classes are Eventual and Eventual* for predefined order and non-deterministic order, respectively. When specifying BART property P1, the user clicks on Select CP on the L boundary frame of the property scope window shown in Fig. 1. This takes the user 11

to the composite proposition screen. Because MB and WS are conditions, the user clicks on the Condition button. The composite proposition used to define the relation between MB and WS is Parallelc because it is necessary to assert both maximum breaking force is applied and wheel slippage is detected.

Figure 5. Composite proposition screen. 4.4. Specifying Common Behavior Manna and Pnueli identify safety, response, and precedence properties as the most common in concurrent systems [16]. Also, a study [6] has identified the response pattern as the most commonly used pattern followed by the universality and absence patterns. These three patterns mapped to 80% of the 580 properties sampled in the study. Because of the frequency with which response properties occur, it’s important to provide abstractions that support multiple propositions when specifying sequence of events or concurrent behavior. Because multiple propositions may occur in the cause and effect part of response properties, composite propositions can be used to assist in their specification and validation. By using composite propositions in either part of the response pattern (the cause or effect), it is possible to represent common behavior associated with concurrent systems, such as synchronized join and fork, concurrency, non-determinism, and sequences. The Select common behavior button, at the bottom of the pattern frame in Fig. 3, enables the screen shown in Fig. 6. 12

Figure 6: Selecting common behavior. Fig. 6 shows names of common behaviors and three different graphical representations for each of them: a) composite proposition symbol, b) timeline diagram, and c) Petri-net. The Petri-net format depicts the essence of the causeeffect relation. Common types of behavior have been identified for multiple propositions that occur in the cause part of the response property. Note that p and q are propositions, and the term activate means becomes true. ƒ Multiple triggers (non-determinism). If (p1 or p2 or ... or pn) is asserted, then some time in the future proposition q is asserted. At least one of the propositions must hold to activate property q. ƒ Synchronized join (concurrency). If propositions (p1 and p2 and … and pn) are asserted at the same point in time, then some time in the future proposition q is asserted. All propositions must hold simultaneously to activate property q. ƒ Consecutive-sequence trigger. If all propositions become true in a specified order in consecutive states, then some future time q must be asserted. A consecutive sequence of events should occur to activate property q. Common types of behavior that have been identified for multiple propositions that occur in the effect part of the response property are described below: ƒ Synchronized fork. If q is asserted, then some time in the future propositions (p1, p2,…, pn) become true at the same time. Properties (p1, p2,…, pn) must not hold when q is asserted. ƒ Parallel assertion (concurrency). If q is asserted, then some time in the future propositions (p1, p2,…, pn) are asserted at the same time. Any of the propositions may hold when q is asserted. 13

4.4.1. Generating Formal Specifications Fig. 7 shows Prospec’s main screen in which specified system properties are summarized. On the top-left frame of the screen, there is a list of names representing elicited properties. For a selected property name, the following information is depicted: natural language description, scope name and its associated CP class(es) for the left and right boundaries, and pattern name and its associated CP class(es).

Figure 7: The property specification screen. The View Formula button allows the user to select a formal language, e.g., FIL or LTL. Prospec generates a formal specification in the language based on the scope, pattern, and composite proposition chosen during the specification process. Buttons New, Edit, View, and Delete in Fig. 7 provide the functionality to maintain the system properties. When a property is added, the user enters the name of the property, English description, scope, and pattern. At any point in the specification process, the user can record any assumptions that are being made about the property. This facilitates validation of the properties and reasoning about the specifications. In accordance with SPS, the specification process involves two steps: the identification of the pattern that corresponds to the program’s intended behavior being specified and identification of the appropriate scope over which the property must hold. Unlike SPS, the steps can be interchanged in Prospec.

5. Generating MEDL Specifications Prospec generates specifications written in a past temporal logic called Meta Event Definition Language (MEDL) [11]. MEDL is used by the Monitoring and 14

Checking (MaC) system [9] to detect at runtime violations of safety properties, which can be written with either conditions or events. 5.1. The Meta Event Definition Language In MEDL, conditions are used to specify invariants, i.e., properties that are true throughout the computation. They are Boolean expressions that have duration. Events represent the occurrence of a given circumstance. They are used to specify alarms, i.e., events that should never occur during the computation. Events do not have duration. Conditions and events can be related. For instance, a condition can be defined by an initial event e1 and a final event e2, written as [e1, e2). An event can be defined using conditions, i.e., the start of a condition or the end of a condition, written as start(C) or end(C), respectively. This work only considers events that are associated to conditions. Conditions are defined recursively as follows. ƒ Every proposition is a condition. ƒ If C1 and C2 are conditions, then !C1, C1 &&C2, C1 || C2, and C1 ⇒ C2 are conditions. ƒ If E1 and E2 are events, then [ E1, E2) is a condition. Events are defined recursively as ƒ If C is a condition, then start(C) and end(C) are events. ƒ If E1 and E2 are events, then E1 || E2 and E1 && E2 are events. ƒ If E is an event and C is a condition, then E when C is an event. MEDL is a past temporal logic that uses the computation up to the current point to determine the truth-value of the formulas. Recall that a computation is a sequence of consecutive states. There is also a valuation function, which, at each state, determines the truth of each condition and the subset of events that are defined. The semantics of MEDL is given in [12]. Let c, g, h, i, and j be conditions and e, e1, and e2 be events. A condition can be used to specify an interval. For instance e1, and e2 may be used to define condition c, denoted [e1, e2). The duration of c represents an interval that starts at the state at which e1 is defined and ends the previous state at which e2 is defined, i.e., it is a left-close and right-open interval. Formula [e1, e2) defines the start and end of the condition. The condition holds when e1 occurs and remains true until e2 occurs. Observe that it is not required that e2 occurs. Events can be used to assert a) the start of a condition, b) the end of a condition, and c) that a condition holds when an event occurs. Event start(c) is defined at state si if c is true at si and c is false at the previous state, si-1. Event end(c) is defined at state si if c is false at si and c is true at si-1. Event end([e1, e2)) specifies the end of an interval. This event is defined at state si if e2 is defined at state si and e1 has been defined at state sj, where j < i. Event formula e when c is defined at state si if e is defined at state si and c is true at si. For instance, formula start([ start(g), start(h))) when c asserts that c is true at the start of interval: [ start(g), start(h) ). 5.2. Mapping Algorithm In order to use MaC to verify specifications written in FIL, it is necessary to map FIL specifications to MEDL. FIL interval formulas assert properties within 15

intervals that must be satisfied, while MEDL alarms detect violations of properties. MEDL makes use of conditions to express safety formulas, a safety property holds during the entire computation. Safety properties can also be written using alarms, i.e., an event that shall not occur during the computation. While FIL interval formulas assert properties that should be satisfied by the system, MEDL alarms assert the violations of properties by the system. The goal of the mapping presented here is to transform safety properties written as an FIL interval formula into an equivalent MEDL formula. In FIL, the interval formula [α | β) p, asserts property p at the beginning of interval [α | β). The interval formula can only be evaluated if the interval can be built. A FIL interval is defined by search patterns α and β and, by definition, can be built if and only if the two searches succeed. In MEDL, an interval is defined by specifying two events, i.e., [e1, e2), where search patterns α and β are represented by events e1 and e2, respectively. MEDL intervals, however, can be built without the occurrence of event e2. To map a FIL interval into a MEDL interval, it is necessary to also assert the end of the interval, e.g., end( [e1, e2) ). To assert property p at the beginning of the interval, property p is asserted when event e1 occurs, i.e., e1 when p. As a result, the mapping from a FIL interval formula to a MEDL formula is [α | β) p ≡ end( [e1 when p, e2) ). This formula asserts both interval [e1, e2) is built and property p is asserted at the beginning of the interval. Since MEDL is used to assert the violation of properties, the intuitive approach is to negate e2. MEDL, however, does not support negation of events. Negation of property p leads to the formula end( [e1 when !p, e2) ) . This formula asserts both that interval [e1, e2) is built and that property p does not hold at the beginning of the interval, i.e., the violation of end( [e1 when p, e2) ). This process does not work for FIL formulas of the form, ¬[α | β) p, since the MEDL formula will result in the negation of an event, i.e., !end( [e1 when !p, e2) ), which is not defined in MEDL. It is necessary, then, to convert formulas into MEDL conditions. The FIL formula [α | β) p is expressed in a condition form by the MEDL formula [ end( [e1 when !p, e2) ), start( [e1, e2) ) ). Since MEDL does not enforce the end of an interval, the complete translation of ¬[α | β) p is ![ end( [e1 when !p, e2) ), start( [e1, e2) ) ). The process to transform an FIL interval formula [α | β) p into a MEDL formula that asserts its violation requires two steps: 1. [α | β) p is transformed into a MEDL condition that asserts its violation as given in formula: [ end( [e1 when !p, e2) ), start( [e1, e2) ) ). 2. The condition expressed in Step 1 is converted into an alarm by asserting its start as denoted by start ( [ end( [ e1 when !p, e2) ), start( [e1, e2) ) ) ). BART property P2, □([→CE | →(TS ∨ NC) ) □ MB), is used to illustrate the application of the mapping algorithm. The following steps are required: 1. Eliminate derived operators, i.e., □ MB, from P2 to obtain the equivalent FIL formula: □ ( [→CE | →(TS ∨ NC) ) [→¬MB | →) false). 2. Change the right search of nested interval [→¬MB | →) to a search to the end of its parent interval: □ ( [→CE | →(TS ∨ NC) ) [→¬MB | →(TS ∨ NC)) false )

16

3. Apply the mapping algorithm to obtain a MEDL condition, and then convert it into an alarm formula by asserting the start of the mapped condition: start([end([ start([ start([ start(!MB), start(TS||NC) ) ∧[ start([ start(CE), start(TS||NC))), start([ start(TS||NC), start(CE) )) )), start([ start(TS||NC), start(!MB) )) )) when true, start([ start([ start(TS||NC)), start(CE) ) ∧[ start([ start(TS||NC), start(!MB) )), start([ start(!MB), start(TS||NC) )) )), start([ start(CE), start(TS||NC) )) ) )), start([start(CE), start(TS||NC) )) ))

The reader can validate that the formula given in Step 3 is an instantiation of the following event formula that asserts the start of a condition: start ( [end( [ e1 when !p, e2)), start( [e1, e2) ) )). The left event of the condition, end( [e1 when !p, e2)), asserts the end of a interval composed by events e1 when !p (outlined in the top box) and e2 (outlined in the middle box). Event e1 when !p asserts the intersection of the left part of the intervals given in Step 2 (→CE and → ¬MB) with the negation of the property to be asserted in Step 2, !false. Event e2 (in the middle box) asserts the intersection of the right part of the intervals given in Step 2, i.e., (→(TS ∨ NC) and → (TS ∨ NC)). Finally, the end of the condition, given by start( [e1, e2) ) (outlined in the bottom box), asserts the beginning of a new parent interval [→CE | →(TS ∨ NC)).

6. Related Work Propel [21] enhances SPS by identifying ambiguities in the intent of the patterns and highlights the aspects of the specification that are open to numerous interpretations, assisting users in making informed decisions. It makes use of disciplined natural language (DNL) and extended finite-state automata to assist in the specification and validation of properties. Scope in the DNL representation is similar to the property-scope decision tree presented in this work. Propel, however, does not handle multiple propositions in the patterns nor in the scopes. In addition, Propel generates a finite-state automaton while Prospec generates a formal specification in LTL and FIL. In Prospec, diagrams that depict the possible computation that may satisfy a given pattern are used to highlight subtle differences in the structure of the patterns. In addition, Prospec use timeline diagrams to highlight the different types of structures for concurrent and sequential behavior when conditions and events are considered. Another approach is the timeline editor tool [22], which specifies response formulas and provides multiple perspectives to the user. This tool uses timeline diagrams and test automata. System responses are depicted in timeline diagrams by specifying temporal relations among events and constraints. The test automaton assists practitioners by providing a different view of the timeline. The creation of both the test automata and Promela code is automated, hiding the formalism from the users. In Prospec, another version of the timeline diagram is used to validate the temporal relations among events and conditions and a formal specification in FIL and LTL is automated.

17

7. Summary Formal specifications of system properties are clearly useful for verifying and validating complex systems. They are underutilized in practice due to the difficulty of creating specifications that are accurate, complete, and nonconflicting. Composite propositions can help practitioners specify and understand properties in a formal language that can be translated for use by existing formal tools. In order to assist in the creation, understanding, and validation of requirements, tools for specifying formal requirements should provide different visual abstractions that present alternative perspectives to the user [4, 15]. In keeping with this philosophy, composite propositions depict relations among propositions using symbols, timeline diagrams and, for response patterns only, Petri nets. As an elicitation approach, composite propositions can highlight subtle details of sequences of events and concurrent behavior by using directed questions to guide the practitioner. Resolving the choices addressed by these questions results in a precise specification of behavior associated to multiple conditions or events. Prospec is based on the Specification Pattern System (SPS). SPS assists property specification by providing patterns of specifications and scopes to restrict the application of patterns. These patterns describe commonly occurring requirements in finite state models of systems. Each pattern describes the structure of specific behavior and defines the pattern’s relationship with other patterns. While property specification patterns assist in the specification of simple properties, they are not able to assist the practitioner in specifying the intended behavior of multiple propositions and the relationships between them. Prospec extends SPS by adding visual representations of patterns, interactively guiding the users during the specification process, and adding composite propositions to assist the user when multiple propositions are used in a pattern or the boundaries of a scope. The composite propositions presented in this paper focus on the specification of common temporal properties. Providing support for these specifications is important because of the ambiguity that multiple conditions or events may have. Composite propositions make the different interpretations explicit. Users are prompted to make informed decisions about subtleties in the structure of the behavior of sequences, and concurrent behavior (concurrency, synchronization, and non-determinism). The proposed extensions will result in tools based on formal semantics and may facilitate the integration of formal approaches into the software development lifecycle. Prospec generates extended FIL and LTL specifications. An automated transformation from FIL safety formulas to MEDL alarms [9] provides support for run-time verification via the MaC system. By automating parts of the formal verification process, Prospec may augment the use of formal methods in software development as suggested in [22]. The work has detected some inconsistencies in property pattern mappings that are in the process of being documented. In addition, it was discovered that MaC can specify properties other than safety, e.g., existence properties where scope does not include the end of the computation.

18

Other work in progress is the use of Graphical Interval Logic (GIL) to provide visual representations of FIL formulas to assist in validation. We are also designing an experiment to measure and analyze the effectiveness of the tool and collect data concerning the applicability of the abstractions.

Acknowledgements This research was partially supported by CONACYT under Contract 68761, NASA grant NCC5-205, NSF grant 26-1005-2, ARL grant DATM05-02-P-0126, and The UTEP Dodson Doctoral Fellowship. The authors want to acknowledge the support provided by Drs. Oleg Sokolsky and Insup Lee with MaC-MEDL and the support provided by Dr. Laura Dillon with GIL and SPS.

References [1] Chang, S., Manna, Z., and Pnueli, A., “Characterization of Temporal Property Classes,” in W. Kuich, editor, Proceedings of the 19th International Colloquium on Automata, Languages, and Programming, LNCS 623, Springer-Verlag, 1992, pp. 474-486. [2] Delgado, N., “A Taxonomy of Dynamic Software-Fault Monitoring Tools,” Master’s Thesis, The University of Texas at El Paso, 2001. [3]

Dillon, L., Kutty, G., Moser, L. E., Melliar - Smith, P. M., and Ramakrishna, Y. S., “A Graphical Interval Logic for Specifying Concurrent Systems,” ACM Transactions on Software Engineering and Methodology, vol. 3, no. 2, April 1994, pp. 131-165.

[4] Dulac, N., Viguier, T., Leveson, N., and Storey, M. A., “On the Use of Visualization in Formal Requirements Specification,” Proceedings of the IEEE Joint Int. Conference on Requirements Engineering (RE’02), Essen, Germany, August 2002, p.p 71-80. [5] Dwyer, M. B., Avrunin, G. S., and Corbett, J. C., “Property Specification Patterns for Finite-State Verification,” 2nd Workshop on formal Methods in Software Practice, Clearwater Beach, Florida, 1998, pp. 7-15. [6] Dwyer, M. B., Avrunin, G. S., and Corbett, J. C., “Patterns in Property Specification for Finite-State Verification,” 21st Int. Conference on Software Engineering, Los Angeles, CA, USA, 1999, pp. 411-420. [7] Gamma, E. and Helm, R., “Design Patterns, Elements of Reusable ObjectOriented Software,” Addison-Wesley, 1995, pp. 416. [8]

Ince, C., “An Introduction to Discrete Mathematics and Formal System Specifcations,” Oxford Univerity Press, New York, 1988.

[9]

Kim, M., Viswanathan, M., et al., "Formally Specified Monitoring of Temporal Properties," in Proceedings of the 11th Euromicro Conference on Real-Time Systems, York, UK, June 1999, pp. 114-121.

[10] Kutty, G., “A Graphical Environment for Temporal Reasoning, ” Dissertation, Electrical and Computer Engineering Department, University 19

of California at Santa Barbara, 1994. [11] Kim, M., Kannan, S., et al., “Java- Mac: a Run-time Assurance Tool for Java Programs,” in Proceedings of Runtime Verification 2001, ENTCS,55(2), 2001. [12] Kim, M., Viswanathan, M., et al., “MaC: A Framework for Run-time Correctness Assurance of Real-Time Systems,” Technical Report, 1998. [13] Lamport, L., Proving the Correctness of Multiprocess Programs, IEEE Transactions on Software Engineering, vol. 3, no. 2, 1977, 125-243. [14] Laroussinie, F. and Schnoebelen, P., “Specification in CTL+Past for Verification in CTL,” Information and Computation, 2000, pp. 236-263. [15] Lecoeuche, R., Mellish, C., and Robertson, D., “A Framework for Requirements Elicitation through Mixed-Initiative Dialogue,” Third IEEE International Conference on Requirements Engineering, Colorado Springs, USA, April 1998, pp. 190-196. [16] Manna, Z. and Pnueli, A., “A Temporal Proof Methodology for Reactive Systems,” in M. Broy (Eds.): Program Design Calculi, NATO ASI 118, Series F: Computer and System Sciences, Springer, 1993, pp. 287-323. [17] Mondragon, O., Gates, A., and Roach, S., “Composite Propositions: Toward Support for Formal Specification of System Properties,” Proceedings of the 27th Annual IEEE/NASA Goddard Software Engineering Workshop, Greenbelt, MD, USA, December 2002. [18] Moszkowski, B., “The Programming Language Tempura,” Journal of Symbolic Computation, vol. 22, no. 6, Dec. 1996, pp. 730-733. [19] Ramakrishna, Y., Melliar-Smith, P, et al., “Really Visual Temporal Reasoning,” in Proceedings of 14th Real-Time Systems Symposium, Raleigh-Durham, NC, 1993, pp. 262-273. [20] Schwartz, R., Melliar-Smith, P., et al., “An Interval Logic for Higher-Level Temporal Reasoning,” in Proceedings of the Second Annual ACM SIGACTSIGOPS Symposium on Principles of Distributed Computing, Montreal, August 1983, pp. 173-186. [21] Smith, R., Avrunin, G., Clarke, L., and Osterweil, L., “PROPEL: An Approach Supporting Property Elucidation,” in Proceedings Int. Conference on Software Engineering, Orlando, FL, USA, May 2002, pp. 11-21. [22] Smith, M. H., Holzmann, G. J., and Etessami, K. “Events and Constraints: a Graphical Editor for Capturing Logic Requirements of Programs,” Sixth IEEE International Symposium on Requirements Engineering, Toronto, Canada, August 2001, pp. 14-22. [23] Winter, V., Berg, R., and Ringland, J., “Bay Area Rapid Transit District Advance Automated Train Control System Case Study Description,” Bhattacharya (eds.): High Integrity Software, Winter, L and Kluwer, S., Academic, Boston, 2001, pp. 115-135. 20