A BRIEF MANUAL FOR VERDECT (Version 2.3) ======================================== VERDECT is a tool to analyze specifications and to verify implementations with respect to a specification. Various correctness conditions can be verified automatically. Both specifications and implementations are given by means of "commands", a language similar to CSP. An implementation is a network of components. A pair of a specification and an implementation is called a decomposition. Each VERDECT session consists of a series of definitions and function calls. A definition binds a command, a network, or a decomposition to a name. Function calls are used to verify correctness conditions of decompositions, display information about a specification or decomposition, and a few other purposes. VERDECT can be used in interactive mode and batch mode. To use VERDECT in interactive mode, simply type verdect The prompt in an interactive VERDECT session is a minus sign (-). To use VERDECT in batch mode, simply type verdect FILE where the file FILE.dec (or FILE) contains all relevant information for verdect. COMMANDS -------- Commands represent sets of finite sequences of atomic actions. A finite sequence of atomic actions is called a trace. For example, the command a?;b! represents the set with the trace of input a followed by output b . Atomic actions always start with a lowercase character. For any symbol b, the atomic command b? represents an input action on b b! represents an output action on b b represents an undirected action on b (sometimes also called an internal action) Furthermore, if C, C0, and C1 are commands, then so are C0 | C1 selection "C0 or C1" C0 ; C1 concatenation "C0 followed by C1" C0 || C1 weaving "C0 and C1" *[ C ] repetition "repeat C any finite no. of times" C^n repetition "repeat C n times, n>=0" |[ A :: C ]| hiding "hide symbols A in C" pref C prefix-closure "take all prefixes of C" ( C ) parenthesize Weaving represents parallel composition with synchronization on common symbols (as in CSP). The list A in hiding is a list of undirected symbols. The binary operators are listed in increasing order of priority. In a command, each symbol must have a unique type, that is, all occurrences are either of type input or of type output or of type undirected. There are two predefined commands, SKIP and ABORT (which may also be written as skip and abort ). SKIP represents the set with the empty trace. It acts as the identity with respect to concatenation and weaving. It is sometimes also referred to as the identity component. ABORT represents the empty set. It acts as the zero element with respect to concatenation and weaving. It is sometimes also referred to as the failure component. STATE GRAPHS ------------ Often specifications are given by means of a state graph. State graphs can be represented in a command as follows. For example, the state graph of a component called WIRE can be specified as state S0 where S0 = ( a? -> S1 ) S1 = ( b! -> S0 ) end The names S0 and S1 are used to represent the two states in the state graph. S0 is the initial state. From state S0 there is a transition on a? to state S1, and from state S1 there is a transition on b! to state S0. All states are final states. The scope of the names S0 and S1 begins with "state" and ends with "end". (So, these names can be reused in another state graph specification.) Here is an example of another state graph. This is a state graph for a JOIN. state S0 where S0 = ( a? -> S1 | b? -> S2 ) S1 = ( b? -> S3 ) S2 = ( a? -> S3 ) S3 = ( c! -> S0 ) end State transitions do not have to consist of a single atomic action. Any command may represent a state transition. For example, the WIRE above can also be specified as state S0 where S0 = ( a?;b! -> S0 ) end Here the command a?;b? represents the transition from state S0 to S0. As another example, the JOIN can also be given by the following expression state S0 where S0 = ( (a? || b?); c! -> S0 ) end where we used the property that (a?;b? | b?;a?) = a? || b?. SPECIFICATIONS -------------- Components are specified by all possible traces they can engage in. Traces are executed one atomic action at a time, starting with the empty trace. As a consequence, trace sets of specifications are prefix-closed, that is, any prefix of a possible trace is possible as well. State graphs, as given above, always represent prefix-closed trace sets. If you are not using state graphs for a specification, you may have to use the pref operator to construct a prefix-closed trace set. For example, the WIRE can be represented also as pref *[ a?;b! ] Without the pref operator, traces like a? or a?;b?;a? are not included in the trace set. By putting the pref operator in front of a command you specify that the traces should be executed one atomic action at a time (instead of sequences of actions at a time). Besides listing all possible traces a component can engage in, a specification also stipulates when an output must be produced. If after a trace an output is enabled in the specification, then an output must be produced. Inputs are under control of the environment and may be produced. In other words, the environment may always stop producing inputs, but the component may only stop producing outputs if no output is enabled. DEFINITIONS ----------- A definition binds a command, a network, or a decomposition to a name. Names must start with a capital; only atomic actions start with a lowercase character. For example, the specification for the WIRE can be bound to the name WIRE by the following definition define WIRE = state S0 where S0 = ( a?;b! -> S0 ) end end If only one state is mentioned in the state graph, you may use the following shortcut. define WIRE = ( a?;b! -> WIRE ) end A command can be parameterized by means of a definition. For example, we can define WIRE(a?,b!) to be a WIRE with input a and output b by means of the definition define WIRE(a?,b!) = ( a?;b! -> WIRE ) end This definition can be instantiated by an expression like WIRE(c?,d!) . When parameterizing a command, all symbols of the command must appear in the list of parameters. NETWORKS --------- A network is a set of component specifications. The component specifications are separated by commas and enclosed in curly braces. For example, a network of two WIREs is given by (using the definition of WIRE(a?,b!) above) { WIRE(a?,mid!) , WIRE(mid?,b!) } Networks can be bound to a name by means of a definition: define IMP = { WIRE(a?,mid!), WIRE(mid?,b!) } end Network definitions cannot be parameterized. DECOMPOSITIONS -------------- A decomposition is a pair of a specification and an implementation satisfying the syntax ( spec=SPEC , imp=IMP ) where SPEC represents a command and IMP a network. For example, using the definitions of WIRE(a?,b!) and IMP from above, the expression ( spec=WIRE(a?,b!) , imp=IMP ) is a decomposition. Decompositions can also be bound to a name by means of a definition: define WIRE_DEC = ( spec=WIRE(a?,b!) , imp=IMP ) end All commands in a decomposition, both in the specification part and in the implementation part, must be prefix-closed, non-empty, and have no undirected symbols. This condition is checked by VERDECT. COMMENTS IN A FILE ------------------ Comments in a file can be placed between /* and */ or on one line after # FUNCTIONS FOR VERIFICATION AND OTHER PURPOSES ---------------------------------------------- In VERDECT, correctness conditions can be verified by calling a certain function. For example, to find out if the decomposition WIRE_DEC has illegal stops, you would type stops( WIRE_DEC ) A list of functions implemented in VERDECT is given below. COM denotes a command and DEC denotes a decomposition. help(): Help information. exit(): Exit VERDECT. env(): Displays all bound names. load("FILE"): Load a file with name FILE or FILE.dec. echo("STRING"): Echo a string to the terminal. show(COM or DEC): Show state graph of command COM or decomposition DEC. size(COM or DEC): Show number of states in state graph of COM or DEC. equal(COM0,COM1): Verify if COM0 equals COM1. closed(DEC): Verify if DEC is closed, that is, there are no dangling inputs or outputs. out_interf(DEC): Verify if DEC has no output interference, that is, no outputs are interconnected. comp_interf(DEC): Verify if DEC has no computation interference (choking), that is, no specification in the decomposition will be violated by any action taken by a component or the environment. safe(DEC): Verify if closed(DEC), out_interf(DEC), and comp_interf(DEC) hold. stops(DEC): Verify if DEC does not have illegal stops, that is, implementation does not stop when specification demands output. int_cycles(DEC): Verify if DEC has no internal cycles, that is, no unbounded sequence of internal actions can occur. complete(DEC): Verify if decomposition is complete, that is, every trace specified may occur in implementation. all(DEC): Verify if DEC passes all tests for a decomposition. Most functions speak for themselves. Here is a brief explanation for some of them. The correctness conditions are explained in the next section. load("FILE") VERDECT will read file FILE.dec. If FILE already ends in .dec, it will read FILE. show(COM) Show the state graph of command COM. The state graph will be printed on the screen in the same format as explained above. The alphabets are given in a comment. Only states reachable from the initial state will be printed. (In case of non-prefix-closed commands, a star (*) in front of a state name indicates a non-final state. All other states are final states.) show(DEC) Show the state graph of all network behaviours of the decomposition DEC. This state graph is the parallel composition of all components in the network and the specification. The state graph is printed only if no computation interference is detected. equal(COM0,COM1) Equality here means COM0 and COM1 have the same input alphabets, output alphabets, and trace sets (i.e., state graphs are equivalent). Should only be used for prefix-closed specifications. ABOUT THE CORRECTNESS CONDITIONS -------------------------------- For each correctness condition, an example is provided in the directory basic-examples that illustrates a violation of that condition. The safety conditions (closed network, no outputs connected, and no computation interference or choking) are well documented in the literature. The liveness or progress conditions (no-illegal-stops, no-internal-cycles, completeness) deserve a few remarks. The no-illegal-stops condition is based on the interpretation that the environment may always stop producing inputs, but the component may only stop producing outputs if no output is enabled in the specification. The no-illegal-stops condition requires that the implementation does not stop producing outputs if an output is enabled in the specification. Although this condition catches many cases of "deadlock", it does not catch the possibility that the implementation goes into an unbounded loop of unobservable actions without ever producing an external output. This unbounded internal behaviour is sometimes called "livelock". The no-internal-cycles condition requires that no unbounded sequence of unobservable actions can be produced by the network of a decomposition. If no illegal stops and no internal cycles are detected, then the implementation is guaranteed to produce an (external) output if the specification demands an output. The completeness condition requires that every trace that occurs in the specification may occur in the decomposition. This condition excludes the possibility of implementing only a proper subset of the traces of the specification. The test for computation interference will build a state graph representing all behaviours the network and environment can engage in. If no computation interference is detected, the number of states of this state graph is given in parentheses. Also, for every 256 states created in this state graph, a dot (".") is printed on the screen. This state graph is used in subsequent tests of no-illegal-stops and no-internal-cycles. During the execution of each of these tests, also a dot (".") is printed for every 256 states visited in the state graph. If any of the above correctness conditions is violated, traces are printed leading up to the violations. STATE EXPLOSION AND STEPWISE VERIFICATION ----------------------------------------- As in all concurrent systems, it is not difficult to find examples that exhibit a state explosion when verifying one of the above conditions. For this reason, it may be handy to know that the safety conditions allow a stepwise verification (or hierarchical verification as it has also been called), provided you always use fresh symbols. That is, if the safety conditions are satisfied by decompositions ( spec=S , imp={ N0, E } ) and ( spec=E , imp={ N1 } ) where N0 and N1 are any lists of components and N0 and N1 only have terminals in common from the alphabet of E, then decomposition ( spec=S , imp={ N0, N1 }) also satisfies the safety conditions. Besides the safety conditions, each of the progress conditions also allows a stepwise verification, provided the safety conditions are satisfied. If you want to avoid a state explosion, you are strongly encouraged to analyze large examples by stepwise verification. DISCLAIMER ---------- VERDECT is free and comes "as is". There is absolutely no warranty. Use it at your own risk. REPORT PROBLEMS OR COMMENTS --------------------------- We know that VERDECT is not perfect and has some problems. We are constantly trying improve it. You may help in this process by sending your comments to us. They will be most welcome. Please write to jebergen@maveric0.uwaterloo.ca SEE ALSO -------- /usr/pa/verdect/examples/ basic-examples/ cant_do/ counterflow/ micropipelines/ /usr/pa/verdect/about.ps /usr/pa/verdect/libraries/