The figure below shows the user interface to the ASTRAL Software Development Environment. The hub of the SDE is the navigation window located in the upper left portion. The navigation window displays the current specification and allows the user to hierarchically traverse it. By double clicking on a line of the displayed specification, a user can move "up" or "down" in the ASTRAL specification hierarchy. For instance, the figure below shows the top level of the Gate process in the railroad crossing specification, which was displayed by double clicking on the "top level" line at the process level. The same effect can be achieved by highlighting a line of the specification and using the up and down arrows. By moving up and down in the navigation window, the corresponding portion of the ASTRAL hierarchy for the current specification is displayed and various functions, such as edit, insert, and remove, can be invoked on the highlighted line of the navigation window. For example, if the "Edit" button was pressed in the figure below, the editor window would pop up with the schedule text loaded. Most of the operations of the SDE are linked in some fashion to the navigation window, either as a form of input or as a form of output.
The top row of buttons in the middle of the SDE are for the most commonly invoked operations in the design phase. The "Status" button brings up the specification manager, which keeps track of changes made to the specification and the current status of proofs. The "Edit" button brings up the syntax-directed editor on the section highlighted in the navigation window. The "Validate" button invokes the specification processing component of the SDE, which brings up a window to report the errors and warnings that result from checking the current specification. By clicking on a result in the error window, the user can move the navigation window to the relevant part of the specification. The "Search" button brings up the search window, which can be used to search and replace expressions throughout the current specification. Finally, the "Split" button invokes the formula splitter, which splits a boolean clause in the navigation window into conjunctive normal form and allows queries to be performed on each split. The lower row of buttons are for commonly invoked operations in the analysis and reuse phases. The "SeqGen" button invokes the transition sequence generator, which displays sequences of transitions that are possible based on a user query. The "ModelCheck" button brings up the ASTRAL model checker, which can prove or disprove system requirements over finite time intervals for a given set of system constants. The "Prove" button generates the PVS translation of the specification and invokes the PVS theorem prover. Finally, clicking on "Compose" allows the user to work with multiple specifications and composition specific clauses.
The browsers in the right portion of the SDE allow the user to execute a number of predefined queries regarding processes, transitions, and variables and their relationships to each other in the current specification. The result of a query can be clicked on to move the navigation window directly to the appropriate location. The status lines at the bottom of the SDE display various items concerning the SDE, such as the specification currently being displayed in the navigation window, the last event of significance in the SDE, and help lines for different items.
Finally, the menu bar between the rows of buttons contains pull-down menus for various operations, including loading and saving specifications, generating proof obligations, setting SDE options (e.g. read-only to assure that a specification does not get modified), and inserting and removing various objects (e.g. processes, transitions, etc.). The separate components of the SDE are discussed in more detail in the following subsections.
The SDE editor provides only the most basic functionality of common general purpose editors such as vi or emacs; however, it is rarely the case that an ASTRAL section is so large as to require the additional functionality provided by general purpose editors. More importantly, the syntax checking, automatic formatting, and on-line syntax documentation of the SDE editor more than compensate for this absence of additional functionality.
All editable items in the SDE are associated with a specific grammar, ranging from the simple alphanumeric constraint on names to the complex grammars of well-formed formulas. Through the use of these grammars, the editor is able to parse its current text and indicate the presence or absence of syntactic errors. The figure below shows the popup window that appears when the edit function is invoked on the section highlighted in the navigation window of the SDE figure. When editing, if the user is unaware of the exact syntax of a section, the "Help" button displays the corresponding grammar and other pertinent information about the section being edited. When the text is correct with respect to its grammar, the "OK" button is displayed at the bottom of the editor. However, when a syntax error is found, the "Parse Error" button is displayed instead, which is the case in the figure below. In addition, the line that is believed to contain the error is underlined, to allow the user to quickly locate and correct syntactic errors. The figure below shows the editor with a parsing error present in the text. The error in this case is a parentheses imbalance. The last line is underlined since that is where the missing right parenthesis causes a syntax error.
When first writing specifications, it is more important to concentrate on the content rather than the readability of the specification. This does not mean, however, that readability is unimportant. In fact, an unreadable specification is likely to contribute unnecessary confusion, errors, and additional time to development. Manual formatting is also likely to impact development time, especially during the initial design stages when changes are more likely to occur. In the same way that word wrap (which is also turned on in the editor for this very reason) in word processors allows writers to concentrate on their words instead of where to place carriage returns, so automatic formatting in the SDE allows specifiers to focus not on how the specification is entered but on what it says. When the OK button is pressed during an edit session, the text in the editor replaces the text the editor was originally invoked on. Before the text is replaced, however, the new text is automatically reformatted into a fixed format.
An advantage of automatic formatting, which is not immediately obvious, is that it allows the user to catch semantic errors that might otherwise go undetected in the specification analyzer. As an example, consider the missing parenthesis in the Gate schedule clause that is shown in the editor window of editor window figure. This parenthesis can be placed in a number of different locations to syntactically fix the problem. Figure (a) below shows the result of formatting in the editor window (after adding the missing parenthesis to the end). As can be seen from this figure, by adding a parenthesis to the end of the text the highlighted implication is placed in the wrong scope. Figure (b) below on the right shows the same formula with the parenthesis correctly placed.
a) b)
Mistaken operator precedence is another type of error that is usually not detectable in the specification analyzer. Therefore, the formatter indicates the precedence of boolean operators by the distance between the operator and its adjoining text. That is, the closer the operator is to the text, the higher its precedence. In the figure below on the left, the highlighted conjunction incorrectly binds more tightly than the two implications surrounding it. In the figure below on the right, however, parentheses have corrected the situation and the conjunction now has a lower precedence than the parenthesized expressions. Both types of errors would most likely go undetected with manual formatting because the user would format the text as s/he assumed it was written, which would be wrong in this case, even though the text was both type correct and syntactically correct.
a) b)
Although the search function is not directly part of the editor, it shares the two features described above. The search button in the main window brings up the search and replace window, which allows the user to search for and replace regular expressions throughout the entire specification or in a specific portion. While there is nothing revolutionary in its behavior, what is important is that even this procedure has been designed to reduce the possibility of error. To assure that the benefits of syntax-directed editing and formatting are not lost, the replace procedure aborts if the replacement text would cause a syntax error within the section where the replacement is to occur. In addition, the text is reformatted appropriately when any replacements are made.
One of the most valuable tools that the SDE has to offer is the validation mechanism, which checks for various static errors in the specification such as type errors. When a specification validates without error, it indicates that the specification is ready for the next stage in its development, namely formal proofs. Similarly, when a composition of system specifications validates without error, it is ready for the construction of the new composite specification.
The bulk of the validation function involves checking that any identifiers used in the specification have been defined in the correct scope and that all operands to both built-in operators and user-defined transitions, defines, etc. have the correct types. Validation also performs other functions such as checking for scope conflicts and warning of missing parameters, which while still well defined in the case of transitions, may not be what the user desired. The figure below shows a sample validation results window, which demonstrates some of the different types of errors that are reported.
In the spirit of "ease of use," entries in the validation window are linked to the navigation window. That is, any error appearing in the validation window can be double clicked, which causes the navigation window to display the corresponding section of the specification and highlight the line at which the error occurred. This is useful for rapidly locating and correcting errors.
The formula splitter converts any ASTRAL well-formed formula into conjunctive normal form and then displays each conjunct separately to the user. The splitter can be invoked on any section of an ASTRAL specification that resolves to a boolean expression. When the splitter is invoked on a section, the splitter window pops up with the splits of that section. For example, consider the splits of the invariant of the P_Robot process in the production cell specification. The figure below shows the window that appears when the splitter is invoked on this formula. The window shows the 16th split of 17. The other splits can be displayed using the up and down arrows at the bottom of the window. Each split displayed is classified according to the property classification criteria of [Kol 99d]. The split in the figure below is a forward liveness property.
The formula splitter also serves as a "formula browser" that allows queries about formulas in the specification to be performed. For example, the user can display the variables used in the current split by performing the "variables..used in Selected Formula". This functionality is described in the browser section.
The process, transition, and variable browsers shown in the figure below and the formula splitter enable the user to view various relationships between the four types of items. To simplify the discussion, let "browser" refer to either the formula splitter or the variable, transition, or process browsers. The queries available in the browsers range from simple queries involving a single step to compound queries involving multiple complex steps. Some simple queries include finding the transitions exported from a process, finding the variables referenced in the entry assertion of a transition, finding the processes that import a variable, and finding the transitions referenced in a formula. More sophisticated queries include finding the transitions that are the predecessors of a transition, finding the formulas that reference a variable in their antecedents, finding the transitions that set the same variables as a transition, and finding the transitions with higher priority than a transition.
In small specifications, the user may be able to determine the results of simple queries manually in a reasonable amount of time. In larger specifications or for more complex queries, however, the difference in speed and accuracy between obtaining the information manually and obtaining it using the browsers will be markedly different. The browsers make use of symbol tables maintained during editing to quickly ascertain and display the appropriate information.
The querying process begins by selecting an item in one of the browsers and pressing the "Query.." button in the corresponding browser, which brings up a pulldown menu with four types of queries. Each query type corresponds to the browser in which the corresponding result of the query will be displayed. Some of the query types are currently empty. For example, the variable browser currently does not have any variable type queries. The transition and process query menus have an additional entry "transition information" and "process information", which brings up a window with the relevant transition or process classifier information as discussed in [Kol 99d].
When a query type is selected, a pullright menu appears with all of the queries of that type. Once a query is selected, the appropriate items are retrieved and are displayed in the browser associated with the query type. Thus, the result of one query becomes the input of the next. Any of the items that appear within the browser windows as the result of the query can be double clicked on to move the navigation window to the item's declaration within the specification. Since a browser may have queries of its own type and sequences of queries may be displayed in a browser whose results were still being used, the query results are stored on a stack in each browser. Thus, for each query, a new frame is pushed onto the appropriate browser's stack and the new query results are stored on the new frame. When a frame is no longer needed, the "Pop" button of each browser can be used to pop the frame and display the new top of the stack.
Since many frames may be on a stack of a browser, it is useful to be able to determine which query created each frame of the stack. The first line of results in each browser indicates the number of the frame, the query the frame was generated by, and the browser and frame number of that browser that the query was invoked on. For example, in the variable browser, a top line of "<>" indicates that the displayed frame is the third frame on the variable browser stack, and that it was generated by the V_EXP query invoked on the first frame of the process browser. The V_EXP query refers the "variables..exported by Selected Process" query.
A browser session can begin in two ways. The most common way is to use the special "processes..defined in specification" query in the process browser, which does not require any browser item to be highlighted. This query displays all levels of all processes declared in the current specification. After this query, the other process browser queries can be used to display items in other browsers. The other way a browser session can begin is to split a formula in the navigation window with the "Split" button as discussed in the formula splitter section. The split formulas that are shown can be queried to display items in other browser.
The browsers in the figure above demonstrate the results of a sample browser session on the railroad crossing specification. First, all processes declared in the specification were listed with the "processes..defined in specification" process browser query. Then, the "variables..declared in or imported by Selected Process" query was performed on the Gate process. Finally, the "transitions..using Selected Variable in an entry clause" query was performed on the train_in_R variable. The end result is a listing in the transition browser window of transitions in which train_in_R appears in an entry clause.
The browsers are especially useful during the maintenance phase, since in many cases it is someone other than the original developer who is responsible for maintaining the specification. In addition, even the original specifier may be unclear on some of the details due to the elapsed time between updates. In either case, the browsers can be used to quickly determine the portions of the specification that may be affected by any proposed changes. For example, suppose that during maintenance the effect that a transition has on some variable needs to be changed. In this case, it is desirable to determine those transitions that may be affected by the change, namely those that use the variable in an entry assertion. Once the transitions are listed with the appropriate browser queries, they can be quickly scanned to determine which ones will be affected by the update.
The browsers can also assist in the proof process. In chapter 9, the browsers are used in a variety of ways during model checker test case generation and proof sketch construction. For example, in the proof of an untimed property "A -> C", the browsers are used to find the transitions that make C false or A true. This is done by first bringing up the property in the formula splitter. To find the transitions that make C false, the "variables..used in consequent of Selected Formula" query is used. Similarly, the "variables..used in antecedent of Selected Formula" query is used to find the transitions that make A true. Once the variables are displayed in the variable browser, the "transitions..using Selected Variable in an exit clause" query is used, which displays the transitions that can possibly violate the property. Any transition that is not listed cannot possible violate the property.
In order to assure that an ASTRAL specification satisfies its requirements, it is necessary to generate and prove the appropriate proof obligations. ASTRAL proofs are divided into three categories: intra-level proofs, inter-level proofs, and composition proofs. The intra-level proof obligations deal with proving that each process level satisfies its stated critical requirements and that the top level specification is consistent and satisfies the global requirements. The inter-level proof obligations deal with proving for each process type that the specification of level i+1 is consistent with the specification of level i. The composition proof obligations deal with proving that the assumptions of each of the components of the composite system are satisfied by the other components in the system that replace what was previously the external environment. Details of the three types of proof obligations can be found in [CKM 94], [CKM 95], and [CK 93], respectively.
The proof obligations for ASTRAL are relatively straightforward, but in many cases are rather lengthy, which means they are prone to error. By generating the appropriate proof obligations automatically, not only is the user relieved of the time involved, but the proof obligations are guaranteed to be accurate. The SDE generates all three types of ASTRAL proof obligations. The intra-level proof obligations have also been encoded in the theorem prover. The inter-level and composition proof obligations, however, have not yet been defined in the theorem prover portion of the SDE, which is discussed later. Thus, until the theorem prover includes these definitions, the user can still obtain the necessary proof obligations by using the verification condition generator (VCG).
The "Status" button invokes the specification manager of the SDE. This tool displays various information about the current specification that is stored whenever a specification is saved. The two main types of information are dates and statuses. The dates indicate when various activities have been performed on the specification. These include the date that the specification has been validated, the dates that different clauses have been changed, the dates that the requirements have been model checked, etc. The statuses indicate what the results of the various activities were. These include whether the specification is valid, whether errors have been found using the model checker, how many proof obligations have been discharged with the theorem prover, etc. The proof manager also displays other information such as the context directory associated with the specification, which indicates where the theorem prover specifications are located. The figure below shows the window of the specification manager.
The information of the specification manager is used by other components of the SDE to perform various functions when needed. For example, most of the advanced components of the SDE, such as the model checker and theorem prover, require that a specification is valid when they are invoked. When a specification is loaded, its validation status is checked. If the specification is valid and has not changed since the time it was validated, the validation procedure is run on the specification so that these advanced components can be invoked immediately after loading. Another component that uses the specification manager information is the transition sequence generator. The sequence generator invokes the theorem prover to attempt the proofs of transition successor obligations, which can be an expensive procedure. The sequence generator uses the transition change dates to determine which transitions have changed since the obligations were last proved. Thus, if only a few transitions have been changed, it is not necessary to rerun the bulk of the transition successor obligations. The change dates are also used when the theorem prover is invoked to determine which portions of the specification need to be translated into the language of the prover. The theorem prover saves specifications that have already been typechecked in a binary form that can be loaded quickly. Since only the portions of the current specification that have changed since the last translation are generated, more of the prover's binary files can be used.
Besides displaying various information about the current specification, the specification manager also directs the user as to which design or analysis step should be performed next. The recommended next step is displayed at the top of the specification manager window as shown in figure above. The recommendation is updated according to the operations that the user has performed on the current specification. The user can invoke the SDE operation that is associated with the recommended step directly using the "Do Next Step" button.
Determining the order in which transitions can fire on a given process is essential to proving that the critical requirements of the process hold. Without this information, it is impossible to determine the transition sequences that can occur on a process, thus it is impossible to determine which states are reachable and which are unreachable. Therefore, it is impossible to guarantee any property of the process. Since sequencing is so crucial to the proof process, it is useful to provide the user with a tool to view the transition sequences that can occur in a given process type. A sequence generator tool is not only is such a tool useful in itself, but it can also be used as the foundation for more complex analysis tools and/or techniques.
For example, a transition sequence generator can be used as the basis for a symbolic executor, which helps the user visualize the operation of the system. To accomplish this, the browsers are first used to determine the transitions that must fire in order to achieve the start state given by the user. The sequence generator is then used to find the sequences of transitions that are possible between the transitions obtained from the browsers. The transition classifier is used to classify the transitions in each sequence to determine whether each transition fires immediately after its predecessor or is delayed according to the current time, the other processes in the system, or the external environment. This time can be estimated by inspecting the entry assertion of the transition and the relevant environment and imported variable clauses. Finally, the path condition of each sequence is constructed by conjoining the entry and exit assertions of all the transitions in the sequence together. The end result is an expression for the process state at each point in the execution of the sequence with an approximate running time up until that point. Other possible uses of the sequence generator will be discussed in later chapters.
Unlike graphical state-machine languages in which the successor information of each transition is part of the specification, in textual languages such as ASTRAL, sequencing cannot be determined without more in-depth analysis. Determining whether one transition is the successor of another in ASTRAL, however, is undecidable since transition entry/exit assertions may be arbitrary first-order logic expressions. Many successors, however, can be eliminated based only on the simpler portions of the entry/exit assertions, such as boolean and enumerated variables. Based on this fact, a transition sequence generator tool has been developed.
The sequence generator is invoked from the actions menu by the "SeqGen" button, which generates sequences for the process level currently being viewed in the navigation window. This action brings up the sequence generator dialog box, which allows the user to direct the construction of the transition sequences. The options include the first and last transitions, the direction to generate sequences from the first transition, the maximum number of transitions per sequence, and the maximum number of sequences. The user must provide the maximum number of transitions per sequence and if the search is backward, must provide the first transition. Once this information is provided, the SDE constructs the sequence generator obligations, invokes PVS, runs the proof scripts, retrieves the results, and then generates the sequences according to the user query. Since running the proof scripts can be time-consuming, the results are saved between changes to the specification, so that sequences can be quickly displayed after the proofs are attempted once.
For each sequence generated, an approximate running time of the sequence is constructed using the transition classifier information. The sum of the durations of all the transitions plus an appropriate delay based on the classification of each transition in the sequence is displayed next to the sequence. A delay produced by the current time is denoted delay_T. A delay caused by other processes in the system is denoted delay_O. Finally, a delay caused by the external environment is denoted delay_E. For delays involving multiple causes, the notations are combined. For example, if a delay is caused by both the current time and other processes, it is denoted delay_OT.
As an example of a sequence generator query, consider the sequences of length seven generated backward from the arrived_at_middle transition of the press of the production cell specification. The figure below shows the sequence generator dialog box and the first of the two sequences that are generated.
The ASTRAL model checker is a highly automated tool that can check a large number of states for violations in the critical requirements. The figure below shows the model checker window that is brought up by clicking the "ModelCheck" button in the SDE.
Since ASTRAL can specify infinite state machines, certain restrictions are needed to limit the number of states explored by the model checker. These include using a discrete rather than dense time domain, restricting the allowed syntax of certain portions of the specification, providing explicit numeric/boolean constants for all symbolic constants, only checking the requirements beginning at the initial state, and providing an explicit number of timesteps to check. Given these restrictions, not all ASTRAL specifications can be model checked. It must first be checked whether the specification meets the syntactic limitations of the model checker. This is done automatically by the SDE. If the specification does not meet the syntactic restrictions, then the model checking portion of the analysis must be skipped. If a specification is syntactically suitable, then the next step is to transform the specification into a form that meets the discrete time domain restriction. This is done by redefining the built-in real type to be an alias type of the built-in integer type. This transformation is performed by the SDE before every model checking session.
Once the dense to discrete transformation has been performed, the model checking procedure is as follows. The user first needs to set up a finite time bound and values for all system or process level constants in the specification by clicking the "Const Setup" button. The time bound indicates the maximal depth that the model checker will search for the current specification. The reason for assigning concrete values to these constants is that currently the model checker can only check a specific instance of the specification. After doing this, the user has two choices for invoking the model checker: "Start(all states)" or "Start(obey Env)". The "Start(all states)" button causes the model checker to enumerate all the possible states within the time bound and to check that the critical requirements of the specification hold in each state. The "Start(obey Env)" button, in contrast, will check only those states that can be reached by satisfying the environment clauses. The default mode of the model checker is to check the system globally. That is, the actual behavior of every system process is modeled. The "Start(Process Level)" button allows each process to be checked modularly. That is, only the actual behavior of a particular process is modeled and the behavior of the other processes is assumed from the imported variable clause of that process.
If a failure is detected by the model checker, the transcript window will indicate the actual detailed trace of the states that violated the requirements of the specification. Each state in the trace contains the truth values of all the critical requirements, the values of all local variables and the status information of all transition instances for every process instance, as well as other information. The user can easily follow the trace to figure out where the specification goes wrong, since each trace is for a single execution branch of the specification and is presented at the specification level. The figure below shows the transcript of a violating trace of states from an earlier version of the railroad specification. Besides performing system level model checking as described above, the model checker can also perform process level model checking by enumerating all reachable states of a process instance. In this case, the states explored are restricted by the imported variable clause of the process.
Interactive theorem provers provide mechanical support for deductive reasoning. To prove the properties of a system with a particular theorem prover, the system and its proof obligations are first expressed in the specification language associated with the prover. The obligations are then discharged by reducing the high-level proofs of the obligations into simpler subproofs using the axioms and inference rules of the prover's specification language. The goal of this reduction is to simplify the proofs enough so that each subproof can be automatically discharged by the prover's basic built-in decision procedures that support arithmetic and Boolean reasoning. Theorem provers provide a number of forms of assistance, which include preserving the soundness of proofs, finishing off proof details automatically, keeping track of proof status, and recording proofs for reuse. Rather than implementing a theorem prover for ASTRAL from scratch, it was decided to take advantage of an existing general purpose theorem prover modified for use with ASTRAL. After investigating a number of theorem provers, the Prototype Verification System (PVS) [COR 95] was considered to be ideal for ASTRAL because of its powerful typing system, higher-order facilities, heavily automated decision procedures, and ease of use.
To use PVS to prove properties of ASTRAL systems, the semantics of ASTRAL needed to be encoded in the PVS logic. These semantics include both the axiomatization of the ASTRAL abstract machine as well as the precise definition of each ASTRAL operator. The abstract machine describes admissible system executions, where a system execution consists of the call, start, and end times of each transition. For example, one axiom of the abstract machine states that if no transition has ended within a given interval on a particular process, then each variable of that process keeps the same value throughout the interval. This axiom is called the vars_no_change axiom and defines the ASTRAL property that variables can only change values when transitions end.
vars_no_change: AXIOM
(FORALL (t1: time, t3: time):
t1 <= t3 AND
(FORALL (tr2: transition, t2: time):
t1 < t2 + Duration(tr2) AND
t2 + Duration(tr2) <= t3 IMPLIES
NOT Fired(tr2, t2)) IMPLIES
(FORALL (t2: time):
t1 <= t2 AND t2 <= t3 IMPLIES
Vars_No_Change(t1, t2)))
Note that the function Vars_No_Change(t1, t2) in the vars_no_change definition is a specification-dependent function constructed by the translator stating that the value of each variable of the process is the same at t1 and t2. The vars_no_change axiom is one of ten axioms in the axiomatization of the ASTRAL abstract machine.
In addition to the abstract machine axioms, the ASTRAL semantics also include the definitions of each ASTRAL operator. Since ASTRAL expressions can have different values depending on the current time in the system (i.e. now), each ASTRAL operator has been defined such that the evaluation of its operands are delayed until a temporal context (i.e. a value of now) is given. For example, the past operator, which normally takes an ASTRAL formula of type T and a time is defined as:
Past(v1: [time -> T], at1: [time -> time])
(t1: {t1: time | at1(t1) <= t1}): T = v1(at1(t1))
When a time is applied to a past expression, the time operand, which can be an arbitrary formula, is evaluated to a specific time and then the value of the formula operand is evaluated at the resulting time. Note that the type of t1 has been limited such that at1(t1) <= t1 to enforce the semantics of the past operator, which says that past cannot be applied at times beyond now (e.g., past(v, now+1) is not allowed). The standard Boolean and arithmetic connectives have been defined similarly to the ASTRAL operators in that their normal operands of type T become functions of type [time -> T]. For example, conjunction is defined as:
AND(b1: [time -> bool], b2: [time -> bool])(t1: time): bool =
b1(t1) AND b2(t1)
With these definitions, expressions in the encoding can be constructed exactly as they are in ASTRAL. When an evaluation time is applied to an expression, the time is propagated to each individual operator and operand in the expression. For example, (A AND B)(t) becomes A(t) AND B(t). The translator component of the SDE can translate any ASTRAL specification into its PVS representation. To translate an ASTRAL expression, its parse tree is traversed and the appropriate PVS definition is substituted for each operator. The two formulas below show the environment clause of the Sensor process in ASTRAL and PVS forms. The left formula is in ASTRAL notation and the right formula is the PVS translation that was automatically generated from the ASTRAL form.
Environment Environment: [time -> bool] =
Call(enter_R, now) & Call1(enter_r, now) AND
EXISTS t: time ( (EX! (t: [time -> time]):
t >= 0 & t >= const(0) AND
t <= now & t <= now AND
Call2(enter_R, t)) -> Calln(const(2), enter_r, t)) IMPLIES
Call(enter_R) - Call1(enter_r) -
Call2(enter_R) > Calln(const(2), enter_r) >
(dist_R_to_I + (const(dist_r_to_i) +
dist_I_to_out) / const(dist_i_to_out)) /
min_speed const(min_speed)
Note that the function "const" is used to denote numeric and symbolic values that are constant over time. When the above expression is evaluated at a specific time, the const "drops out". Also note that user-defined identifiers such as "enter_R" have been changed to a lower case form in the translation. This is because PVS is case-sensitive while ASTRAL is case-insensitive, thus the choice was made to always translate user-defined identifiers into a lower case form. The axiomatization and the operator definitions have been incorporated into an ASTRAL-PVS library, included as part of the SDE. For a complete description of the axiomatization and the PVS encoding, see [Kol 98].
Although ASTRAL allows individual specifications to be composed into a new composite specification, the extensive amount of work required to build the new specification (as described in [CK 93]) may cause users to hesitate before taking advantage of this feature. Also, when constructing the composite specification there are numerous opportunities for errors and omissions. By using the SDE, however, the user is completely relieved of the burden of constructing the new specification.
The "Compose" button sets the SDE into composition mode and allows the manipulation of multiple system specifications in the same fashion as individual specifications by adding a new topmost level to the ASTRAL hierarchy, which contains specifications as its components along with composition specific clauses. The figure below shows the additional composition hierarchy. When validating a composition, the validation procedure examines the declarations in all specifications and warns the user of possible name conflicts. Those declarations that have the same name but different meanings between specifications can be changed by the user using the search and replace feature. Declarations with the same meaning can be left as is and duplicates will be removed automatically during the construction of the composite specification.
When the SDE is in composition mode, the compose button is replaced by a "Build" button. The build procedure performs a number of transformations to construct the new composite specification. For example, call statements involving exported transitions that have been made internal must be replaced by an expression derived from the corresponding call generation clause describing how the transition is invoked internally. However, the call generation clause cannot simply be used as it is declared because it is written for all calls in the system whereas the calls being replaced are specific instances with a particular process id, time, and parameters as well as possibly referencing a number of calls into the past (i.e. using Calln where Calln(T, t) holds if the nth call in the past to transition T occurred at time t).
Similar changes need to be made for the environment clauses. That is, the environment is required to satisfy certain conditions to guarantee correct behavior of the system, but when an exported transition becomes internal, assumptions about calls to that transition must now be satisfied by the behavior of other processes in the system rather than by the external environment. Thus, those assumptions must be moved from the environment section to the imported variable clause. This process is performed with the assistance of the formula splitter.
Besides replacing calls with equivalent call generation expressions and moving environmental assumptions to the imported variable clause, the build procedure also performs other transformations. These include removing the no longer exported transitions from the export clause, importing any variables, types, etc. used in the modified clauses, and updating transition entry/exit assertions. In fact, the build procedure performs all of the transformations discussed in [CK 93]. Thus, the user is completely relieved of the burden of producing the composite specification by the build function of the SDE.
| [CK 93] | A. Coen-Porisini and R.A. Kemmerer. "The composability of ASTRAL realtime specifications". International Symposium on Software Testing and Analysis, Cambridge, MA, USA, 28-30 June 1993. SIGSOFT Software Engineering Notes, July 1993, vol. 18, (no. 3): 128-38. |
| [CKM 94] | A. Coen-Porisini, R.A. Kemmerer, and D. Mandrioli. "A formal framework for ASTRAL intralevel proof obligations". IEEE Transactions on Software Engineering, Aug. 1994, vol. 20, (no. 8): 548-61. |
| [CKM 95] | A. Coen-Porisini, R.A. Kemmerer, and D. Mandrioli. "A formal framework for ASTRAL inter-level proof obligations". Proceedings of the 5th European Software Engineering Conference, Sitges, Spain, 25-28 Sept. 1995. Berlin, Germany: Springer-Verlag, 1995. p. 90-108. |
| [COR 95] | J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas. "A Tutorial Introduction to PVS". Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, Apr. 1995. |
| [Kol 98] | P.Z. Kolano. "A Theorem Prover for ASTRAL". Technical Report TRCS98-01, Computer Science Department, University of California, Santa Barbara, Jan. 1998. |
| [Kol 99d] | P.Z. Kolano. "Tools and Techniques for the Design and Systematic Analysis of Real-Time Systems". Ph.D. Thesis, University of California, Santa Barbara, 1999. |
Richard Kemmerer / kemm@cs.ucsb.edu
URL: http://www.cs.ucsb.edu/~astral/tools.html
last update: 7-27-99