Engineering formal requirements:an analysis and testing method for Z documents Paolo Ciancarini Stelvio Cimato Cecilia Mascolo

Technical Report UBLCS-96-6

March 1996

Department of Computer Science

University of Bologna Piazza di Porta S. Donato, 540127 Bologna (Italy)

The University of Bologna Department of Computer Science Research Technical Reports are available ingzipped PostScript format via anonymous FTP from the area

ftp.cs.unibo.it:/pub/TR/UBLCS or viaWWW at URL http://www.cs.unibo.it/. Plain-text abstracts organized by year are available in thedirectory ABSTRACTS. All local authors can be reached via e-mail at the address last-name@cs.unibo.it. Questions and comments should be addressed to tr-admin@cs.unibo.it.

Recent Titles from the UBLCS Technical Report Series

94-14 A Comparison of Parallel Search Algorithms Based on Tree Splitting, P. Ciancarini, May 1994. 94-15 RELACS: A Communications Infrastructure for Constructing Reliable Applications in Large-Scale DistributedSystems, "O. Babao*glu, M.G. Baker, R. Davoli, L.A. Giachini, June 1994.

94-16 Replicated File Management in Large-Scale Distributed Systems, "O. Babao*glu, A. Bartoli, G. Dini, June1994. 94-17 Parallel Symbolic Computing with the Shared Dataspace Coordination Model, P. Ciancarini, M. Gaspari,July 1994. 94-18 An Algorithmic Method to Build Good Training Sets for Neural-Network Classifiers, F. Tamburini, R. Davoli,July 1994. 94-19 On Group Communication in Large-Scale Distributed Systems, "O. Babao*glu, A. Schiper, July 1994. 94-20 Dynamic Allocation of Signature Files in Multiple-Disk Systems, P. Ciaccia, August 1994. 94-21 Parallel Independent Grid Files Based on a Dynamic Declustering Method Using Multiple Error CorrectingCodes, P. Ciaccia, November 1994.

95-1 Performance Preorder and Competitive Equivalence, F. Corradini, R. Gorrieri, M. Roccetti, January 1995(Revised December 1995). 95-2 Clepsydra Methodology, P. Ciaccia, O. Ciancarini, W. Penzo, January 1995. 95-3 A Unified Framework for the Specification and Run-time Detection of Dynamic Properties in DistributedComputations, "O. Babao*glu, E. Fromentin, M. Raynal, January 1995 (Revised February 1995).

95-4 Effective Applicative Structures, A. Asperti, A. Ciabattoni, January 1995. 95-5 An Open Framework for Cooperative Problem Solving, M. Gaspari, E. Motta, A. Stutt, February 1995. 95-6 Considering New Guidelines in Group Interface Design: a Group-Friendly Interface for the CHAOS System,

D. Bottura, C. Maioli, S. Mangiaracina, February 1995.

95-7 Modelling Interaction in Agent Systems, A. Dalmonte, M. Gaspari, February 1995. 95-8 Building Hypermedia for Learning: a Framework Based on the Design of User Interface, S. Mangiaracina, C.Maioli, February 1995.

95-9 The Bologna Optimal Higher-Order Machine, A. Asperti, C. Giovannetti, A. Naletto, March 1995. 95-10 Synchronization Support and Group-Membership Services for Reliable Distributed Multimedia Applications,F. Panzieri, M. Roccetti, March 1995 (Revised July 1995).

95-11 The Inherent Cost of Strong-Partial View-Synchronous Communication, "O. Babao*glu, R. Davoli, L.-A.Giachini, P. Sabattini, April 1995. 95-12 On the Complexity of Beta-Reduction, A. Asperti, July 1995. 95-13 Optimal Multi-Block Read Schedules for Partitioned Signature Files, P. Ciaccia, August 1995. 95-14 Integrating Performance and Functional Analysis of Concurrent Systems with EMPA, M. Bernardo, L.Donatiello, R. Gorrieri, September 1995.

95-15 On Programming with View Synchrony, "O. Babao*glu, A. Bartoli, G. Dini, September 1995. 95-16 Generative Communication in Process Algebra, P. Ciancarini, R. Gorrieri, G. Zavattaro, October 1995. 95-17 Dynamic Declustering Methods for Parallel Grid Files, P. Ciaccia, A. Veronesi, November 1995. 95-18 Failure Detectors, Group Membership and View-Synchronous Communication in Partitionable AsynchronousSystems (Preliminary Version)

, "O. Babao*glu, R. Davoli, A. Montresor, November 1995.

96-1 An Investigation on the Optimal Implementation of Processes, C. Laneve, January 1996. 96-2 Expansivity, Permutivity, and Chaos for Cellular Automata, F. Fagnani, L. Margara, January 1996. 96-3 Enriched View Synchrony: A Paradigm for Programming Dependable Applications in Partitionable Asyn-chronous Distributed Systems, "O. Babao*glu, A. Bartoli, G. Dini, February 1996.

96-4 May and Must Testing in the Join-Calculus, C. Laneve, March 1996. 96-5 The Shape of Shade: a Coordination System, S. Castellani, P. Ciancarini, D. Rossi, March 1996.

Engineering formal requirements: an analysis and testing method for Z documents

Paolo Ciancarini1 Stelvio Cimato1 Cecilia Mascolo1 Technical Report UBLCS-96-6 March 1996

Abstract Z is a declarative, not executable specification language; its diffusion in the field of requirements engineeringoutside academia is slow but growing. In this paper we study some methods for analyzing and testing Z

specification documents, with special emphasis on methods for analyzing and animating non sequentialsystems. We describe two techniques we have developed to analyze Z documents specifying non-sequential systems. The first technique allows one to add to the requirements document a number of properties thatthen can be checked using a formal semantics; the second technique allows to obtain directly from the requirements specification document by refinement and compilation a distributed prototype that can beexecuted and tested over a network of workstations.

1. Department of Computer Science, University of Bologna, Via Mura A. Zamboni, 7, 40127 Bologna, Italy

1

1 Introduction 1 Introduction The Z notation [Spi92, BN92] has been used as a specification language to formally describe andanalyze the requirements and the design architectures of a wide range of hardware and software

systems; for some examples see [Hay93]. However, Z has been successfully used especially forthe specification of sequential systems rather than concurrent systems. Since Z is an extremely abstract specification language, specifiers of concurrent or distributed systems have very poorsupport and need to pay special attention to behavioral aspects of their formal documents.

In fact, even if in the recent years Z has been sometimes used for specifying concurrent, re-active, or even distributed systems [Hay93], in general non-sequential systems are difficult to be fully described and analyzed using Z. A number of researchers have attempted to overcomethe difficulties, typically combining Z with some other formalism well suited to specify dynamic properties. Thus, combinations of Z with either Petri Nets [vSV91, He95], temporal logic[CDD

+89], or TLA [BL95] have been studied. Usually no tool is given to support the engineering

of formal requirements written in these hybrid notations, except maybe a syntax checker basedon a LaTeX-like concrete syntax.

The approach we present here offers the specifier two complementing approaches for analyz-ing, testing, and validating the formal requirements specification of a concurrent system. The first approach allows a formal analysis of a Z document: its dynamics is formally expressedand studied on an execution model, to be considered a sort of abstract symbolic execution in the sense of [Kem85]. The second approach consists of using a tool for automatic generation of adistributed prototype of the system which makes practical animating the specification in order to debug it from errors, inconsistencies, and ambiguities in a truly concurrent framework.Z has a very abstract, declarative semantics [Spi92]. We introduce a new operational semantics: it is based on the chemical metaphor embedded in the notation of the Chemical Abstract Machine[BB92], which itself has been recently proposed as a specification notation [IW95]. We define on such a semantics a logic offering a number of constructs which can be used to define andanalyze dynamic properties. Moreover, the semantics has been used also to design a tool that is a parallel animator: it consists of a source-to-source translator which compiles a Z document intoa program written in the concurrent language Shared Prolog, which has a chemical semantics as well. The resulting animation can be executed in a distributed environment to make observablethe concurrent behaviors of the system being specified.

This paper has the following structure: Sect.2 shortly introduces Z and surveys the main toolsa requirements engineer can use to validate a formal requirements document. Sect.3 describes our analysis techniques discussing a simple example with concurrency features we will use inthe rest of the paper. Sect.4 describes the formal operational semantics and the logic we use to analyze Z documents. Sect.5 discusses the concept of animating a Z specification; in Sect.6 andSect.7 we discuss an actual animation and its refinement. Finally, in Sect.8 we describe some related and current work.

2 Using the Z notation for requirements engineering We see the specifier as an expert in formal methods who acts on behalf of the customer. Specifiersare different from designers in that they do not deal with architectural or organizational issues.

The specifier writes a formal requirements document cooperating with the user.At this step, a first statement of the problem to be analyzed is given by means of the presentation of the general framework to be subsequently implemented. The accuracy in the descriptionof the required system has great importance, especially because it helps in avoiding errors that would be more expensive to correct if discovered in subsequent phases. Any error found by thespecifier at this stage requires a reformulation of the specification, limiting the required modifications at a very high abstraction level. Any requirements inconsistency or incompleteness foundat subsequent stages in the development process could imply a redefinition of the initial specification document, thus affecting the whole development process [Kem85]. The use of formal UBLCS-96-6 2

2 Using the Z notation for requirements engineering notations and tools during this phase ensures a rigorous approach to requirements analysis byobtaining coherent, complete, correct, and unambiguous specifications.

We now shortly survey Z and the tools that a specifier can use to improve confidence in hisrequirements document.

2.1 The Z Notation Z is a formal specification language based on set theory and first-order logic [Dil90, Spi92]. A Zspecification includes a set of entities, called schemas representing either abstract states of a system

being specified or operations on them. The specification outlines an abstract model defined bymeans of typed entities and their related operations, expressed through a rich set of mathematical constructs.A schema consists of a declarative part (the signature), where data structures, variables, and other schemas can be included, and a predicative part consisting of assertions, properties, andinvariants. For instance, Fig. 1 shows four Z schemas specifying a Buffer. In this example, the invariant specified in the Buffer schema states that the buffer cardinality is less than some limit.

Buffer buffer : ff(MESSAGE ) limit : fl

#buffer ! limit

Init Buffer Buffer0

buffer0 = OE limit0 = 10

Produce \Delta Buffer m? : MESSAGE

buffer0 = buffer [ fm?g

Consume \Delta Buffer m! : MESSAGE

m! 2 buffer buffer0 = buffer n f(m!g

Figure 1. A simple Z specification There are two basic kinds of schemas: those describing abstract data structures and thoserepresenting operations on them. The description of an operation is based on the concept of predicate on state transformation, that is a logic formula including a pre-state and a post-state.Schemas which "change" the state are marked by the presence of the

\Delta  operator, while schemaskeeping unchanged the current state of the system are marked with the

\Xi  operator. Initializationschemas allow for the definition of only post-states by simply providing primed signatures in

UBLCS-96-6 3

2 Using the Z notation for requirements engineering their declarative part (see the Init schema definition in Fig. 1). The Z description of abstract datastructures is given by means of schemas in which no

\Delta  or \Xi  inclusions are present.Variables ending with "?" represent input data, while those ending with "!" represent output.

Furthermore, primed variables represent the state after an operation whereas unprimed onesdenote the before state.

A major feature of Z is the schema calculus, that is a way of composing schemas. It uses somespecial symbols describing how different parts of the specification document can be combined together (sequential composition, parameter passing, combination through logical connectives,etc.). For a detailed description of the Z notation the reader should refer to [Spi92].

2.2 The Role of Tools We concentrate on the process that starts from a formal requirements document and producesa validated specification. Ideally, a number of tools can help the requirements engineer during

such a process:

ffl Pretty printers and text formatters, to improve readability and to provide indexing. Forinstance, Z has a L

ATEX-based syntax, that immediately compiles with TEX.

ffl Type checkers, to verify consistency in a specification document containing typed entities.For instance, fuzz is a type checker of Z documents written in L

ATEX[Spi88a].

ffl Theorem provers, which help in proving formal properties to improve confidence in theircorrectness [BG94, BKKT95].

ffl Model Checkers, automatic tools for analyzing state machines by exhaustive search of theirstate spaces; for instance, Nitpick is a model checker for a subset of Z [Jac94, DJ96]. ffl Animators, that are tools to compile and execute specification documents written in non-executable formal languages. Animators support rapid prototyping, but are also helpful in

proving that a specification is really implementable; some sequential animators for Z aredescribed in [DKC89, SCT96]. ffl Test case generators, namely tools able to generate test suites directly from specifications,that then can be used by programmers to test and debug the real implementation; a test

case generator for Z is described in [RAO92].Pretty printers and type checkers are the first tools a specifier can use to parse and check a Z document. Type checkers like Fuzz [Spi88a] or ZTC [Jia94] determine if a Z specification is bothsyntactically correct and correctly typed.

Unfortunately, parsers and type checkers are not sufficient to guarantee the correctness of thespecification. They can detect mistakes like misusing a variable but they cannot reveal semantical inconsistencies. For instance, consider the Buffer specification and the following new operation:

OverProduce \Delta Buffer m? : MESSAGE

#buffer = limit \Gamma  1 buffer0 = buffer [ fm?g

OverProduce inserts a message in the buffer when its cardinality is limit \Gamma  1. The schema isclearly inconsistent with the

Buffer schema (in fact it does not satisfy the invariant) however thetype checker is unable to reveal violation. Consider again the

AddBuffer operation: suppose thespecifier forgot to put ' after the first buffer: the checker successes in checking the schema anddoes not report any errors.

The analysis of types cannot alone justify the effort of formalizing a specification. There mustbe some means of investigating details of behavior [Jac94]. Specification verification is a process that should be used to check whether a specification is correct in some sense [BSC94]. It involvesrigorous, formally justifiable proofs: for example that a specification is internally consistent.

In order to verify the product quality, very important tools are theorem provers, becausea formal document should be proved correct with respect to the requirements specification.

UBLCS-96-6 4

3 A concurrent specification: a lift system Theorem provers allow for automatic and detailed analysis of specification documents. Morespecifically, provers for Z provide automatic computation of preconditions of operations checking whether the operations are feasible, or if there is consistency between pairs of schema predicates.For instance, calculating the precondition of the operation

OverBuffer shows that the specificationis inconsistent: in fact,

pre OverBuffer is #buffer = limit \Gamma  1 ^ #buffer ! limit \Gamma  1. Theorem provers also help in revealing what is implicit in the specification: a fully formalproof gives a much higher level of confidence in the specification, but at a price. The Z/Eves system [Saa89] provides a theorem prover (Eves) able to deal with Z documents:Z code is translated in the first order predicate calculus supported by Eves; a drawback of this prover is the amount of machine time taken to compute proofs [BG95]. The HOL theorem proverenvironment has been used for analyzing Z documents as well: in this case Z code has to be translated into higher order logic (HOL) before being processed. Though HOL system has betterperformance, it is less automatic than Eves: more user interaction is requested to complete proofs.

Unfortunately, the effort needed to prove a property of a specification formally is far greaterthan that for writing it [BSC94]. Automatic provers usually need much help from specifier that often must suggest the way the prove should progress. Guiding a theorem prover calls fora mathematical sophistication (and investment of time) that most users do not have, so these tools have been mostly confined to experts working in areas that can afford the cost, such assafety-critical software [Jac94].

Model checking calls for no user guidance (like type checking), but like theorem proving,it can answer quite sophisticated queries. However, model checking works on only finite state machines and most software systems have infinitely many states. The rationale behind whytheorem proving has been primary approach for reasoning about software systems is that software systems are, in general, infinite state machines. In [Jac94] model checking is successfully used onsoftware systems with infinite states: the idea is to build an abstraction in which a small number of abstract models represents a large (possibly infinite) set of concrete models. For instance, thetype

Int can be abstracted to fj neg; zero; pos jg. Abstraction can be used to automate the proof ofsome simple theorems usually proved by hand.

To state a property that guarantees a safe behavior of the buffer, for instance "a message producedwill eventually be consumed", we need to specify the buffer's dynamic behavior. Z declarative semantics does not allow to define a concept of "history", so a property like the one definedabove cannot be defined. In fact, no existing tools for Z can perform analysis on dynamic aspects of the system being specified.A language derived from Z, namely Object-Z [CDD

+89], allows temporal properties to be

specified, introducing a trace-based semantics. We are here interested in original Z, so that wecan continue to use all the existing tools and techniques.

3 A concurrent specification: a lift system In order to explain our approach we use a well known example: the Lift System [GGMM87,Eva94a, RAO92, CWB94].

3.1 Informal requirements specification A lift controller system has to service requests coming from the buttons placed on the floors of abuilding. A lift is moved by the controller in a direction satisfying the pending requests until no

more requests are found; in this case the lift changes direction to service other new or pendingrequests.

3.2 Formal requirements specification In [Eva94a] the requirements for a lift system are specified using Z; a number of dynamic propertiesare stated using some Unity-like logic constructs [MM88]. Although the use of Unity logic allows

UBLCS-96-6 5

3 A concurrent specification: a lift system to capture dynamic properties not directly expressible in Z, the intended operational semanticmodel is strongly underspecified and the analysis method is unclear. Instead, we will formalize both an operational semantics and a logic suitable to reason on it.To substantiate our approach we use the same version of the lift problem given in [Eva94a]. Although our specification is very similar to the original, the interpretation we associate to it iscompletely different.

We start the specification introducing a number of free types, namely primitive types definedby enumeration.

DIRECTION ::= up j down STATE ::= stopped j moving DOOR ::= open j closed REQUEST TYPE ::= up request j down request

Using Z free types we state that DIRECTION can be up or down, while STATE is stopped ormoving,

DOOR can be open or closed, and REQUEST TYPE is up request or down request.A lift can be defined by its position, direction, state, and door state:

Lift position : fl direction : DIRECTION state : STATE door : DOOR

The following schema describes a lift system, which includes a lift and some requests:

Lift System Lift requests : ff(REQUEST TYPE \Theta  fl)

requests is the set of requests indicating their type and floor.The initialization operation schema is:

Init Lift System Lift System0

position0 = 1 direction0 = up state0 = stopped door0 = open requests0 = OE

The operation schema Make Requests adds a new request to the requests set.

Make Requests \Delta Lift System r? : REQUEST TYPE f ? : fl

requests0 = requests [ f(r?; f ?)g

The schema describing the moving of the lift up (a single schema in [Eva94a]) is here dividedup in two schemas, namely

Move Up Up and Move Down Up. In this way we avoid . operatorin schemas and obtain simpler rules in the semantic mapping (see Sect.4.1).

UBLCS-96-6 6

3 A concurrent specification: a lift system Schema Move Up Up describes the moving up of the lift when up requests are present abovethe lift's current position; it applies only when the lift is already moving "up".

Move Up Up \Delta Lift System

door = closed (9 f : fl j (up request; f ) 2 requests ffl f ? position) direction = up position0 = position + 1 direction0 = up state0 = moving door0 = closed

Operation schema Move Down Up defines the operation of changing the direction from downto up if no more down requests are present under the current position and there is at least one request for the lift above its position.

Move Down Up \Delta Lift System

door = closed (9 f : fl j (up request; f ) 2 requests ffl f ? position) direction = down : (9 fl : fl j (down request; fl) 2 requests ffl fl ! position) position0 = position + 1 direction0 = up state0 = moving door0 = closed

Move Down Down and Move Up Down are the specular schemas for the moving of the liftdown, which we do not report here for conciseness. The other operation schemas are

Open Doorand Close Door which respectively describe the operation of opening the door when requestsare present at the current floor and the operation of closing the door after having served some

requests.

3.3 Formal analysis Given the above formal document, suppose we intend to analyze it, looking for possible errors orinconsistencies. We need to "interpret" the document, especially if we are interested in properties

of its intended dynamics.In order to express properties on the dynamic behavior of the system, Unity-like logic constructs are introduced. Liveness (namely "a good thing will eventually occur") or safety (namely"a bad thing never happens") properties can be expressed in this way.

Properties are predicates (as the ones in the operation schemas) built using some logic opera-tors (

^, ., : , ,, )) and Unity constructs stated out of every operation schema (we will formallydefine the new logic constructs and analyze the properties given above in Sect.4.3).

Example We state some properties about the Lift system [Eva94a]

1. Theorem 1: Invariant door = open ) state = stopped

2. Theorem 2: (t; f ) 2 requests ^ f = position ^ door = closed

ensures door = open

UBLCS-96-6 7

4 Specifying the dynamics of Z specifications 3. Theorem 3: (r; f ) 2 requests ^ r ? position ^ direction = up

^ state = moving ^ door = closed leads to position = r

The first theorem states that in every moment if the door is open then the state of the lift isstopped. The second one ensures that when the lift arrive to a floor where requests are presents it opens its door. The third one means that when the lift is moving up and there are requests aboveits position, it will eventually satisfy them arriving at the floors requested.

Question is: are these properties true or false given the Z specification? To answer to this kindof questions is the goal of the formal analysis we describe in the next sections.

4 Specifying the dynamics of Z specifications Before giving semantics to Z constructs we define the relevant syntactical elements of a Z specifica-tion. The elementary components of any Z document are State schemas and Operation schemas.

This means that we can see a Z specification as a pair: ! S ; O ? where S is the set of the Stateschemas and

O the set of the Operation schemas. Semantically, a State schema s in S can be seenas the set of all its possible instantiations [Spi88b]. The standard Z semantics [Spi88b, BN92, BB94]

is declarative and does not offer any formalization for concurrency. Thus, we have defined anoperational semantics based on a chemical model.

For simplicity and conciseness, here we consider a restricted version of Z; we specify such afragment using Z itself, thus following the Z tradition [Spi88b, GLW90]. Moreover, because of the concurrent interpretation of Z that we are going to give, we make the following assumption:all variables not explicitly mentioned in the postconditions of an operation schema need not to be invariant (that is: other operations can concurrently modify them). This assumption is neededin our interpretation and allows concurrency of the operations. In some papers on analysis of Z documents the assumption is exactly the opposite: "Variables not mentioned in the schemas areconsidered unchanged": e.g. [RAO92]; however, this is not standard Z too.

We remark that our assumption, together with the suppression of the invariants Lift0 = Liftfrom

Make Requests operation and Requests0 = Requests from Move Up Up and Move Down Upallows concurrency among operations acting on the

Lift and operations acting on the Requests.In the Chemical Abstract Machine (CHAM) model [BB92] Molecules, Solutions, and Rules are

the fundamental elements. A Chemical Abstract Machine is a triple (G; C ; R) where G is agrammar, C is a set of configurations (the language generated by the grammar) or molecules, and R is a set of the rules condition(C ) \Theta  bag C \Theta  bag C . A solution is a multiset of molecules: bag C .In the Chemical Abstract Machine two rules can fire concurrently if they do not need the same molecules to react on; hence, several rules can progress simultaneously on a solution. If two rulesconflict, in the sense that they "consume" the same molecules, the choice of which to let react is non deterministic.A CHAM has some similarities with a Z specification. The state of a Z specification is global, even if it can be seen as a composition of many sub-states, corresponding to the stateschemas involved in the specification. Using the CHAM the global solution is composed of several completely independent sub-solutions. Moreover, in both Z and the CHAM the firing ofactions cannot be enforced; there are only enabled or not enabled operations (or rules). In fact Z operations are enabled when their preconditions are satisfied and CHAM rules are enabled whenconditions are true and molecules in the left-hand side of the rule are present.

We consider a fair CHAM where repeatedly enabled rules will eventually be fired: in this wayit is possible to capture eventual executions.

4.1 An Operational Semantics for Z We give a CHAM interpretation of Z specifications which allows us to deal with concurrentdynamics.

Intuitively, an instance of a state schema is associated to a solution (inst " ff(C )) where, insome way, each variable is a subsolution (in many cases a single molecule). Instead, an operation

UBLCS-96-6 8

4 Specifying the dynamics of Z specifications schema corresponds to a chemical rule where premises and consequences are solutions composedof pre and post conditions of the operation.

We describe the formalization of such an interpretation using the Z language itself.A molecule is a tuple of a name, a type and a value:

MOLECULE == NAME \Theta  TYPE \Theta  VALUE A solution is a bag of molecules:

SOLUTION == bag MOLECULE and a rule is composed of a conditional part that define the applicability of the rule and of twosolutions to indicate molecules to delete and add to the state solution:

RULE == CONDITION \Theta  SOLUTION \Theta  SOLUTION We will call the first SOLUTION "pretuples" and the second "posttuples" so to avoid mis-matching. A rule is applicable to a solution if the solution contains molecules that satisfy the conditionalpart (

CONDITION ) of the rule and molecules that match the pretuples of the rule.The function

FSem associates a solution to a schema instance:

Fsem : SCHEMA INSTANCE " SOLUTION Every identifier of the schema instance is associated to a subsolution (not necessary a singlemolecule): we remark that Z sets and bags are decomposed by this function in several molecules

so to increase potential concurrency of the model.

Fsem op associates a rule to an operation schema 2:

Fsem op : SCHEMA OP " RULE Fsem Op associate to pre and postcondition of a schema different part of the rule:

ffl Every Z schema postcondition that specifies the removal of an element from a set or bag ismapped on a pretuple of the rule (molecule to be deleted).

ffl Every postcondition that specifies the insertion of an element in a set or bag is mapped ona posttuple of the rule (molecules to be added). ffl Every Z precondition that defines a membership (2, \Phi ) is mapped on a pretuple (a removal)and also on a posttuple (reinsertion) if Z postcondition do not contain an indication of

removal of that element: in other words a check of membership is seen as a removal andreinsertion. ffl Postconditions containing mathematical operators (+, \Gamma ,..) on naturals are encoded deletingone molecule and adding the molecule updated.

Example: x 0 = x + 1 is seen as (x ; fl; v) in pretuples and (x ; fl; v + 1) in posttuples of therule. ffl Preconditions containing relational operators (!,?) are encoded as conditions, but themolecule corresponding to the variable is deleted and readded as already described 3.

Example: x ! 5 is seen as v ! 5 " (x ; fl; v) ) (x ; fl; v)Now, following the interpretation of the chemical machine, rules can fire concurrently when

they are enabled by conditions and non conflicting on pretuples molecules.It is now possible to define many other functions to describe, for instance, when rules, i.e. operation schemas, can fire concurrently: it usually depends on their postconditions.

2. A similar function has been defined for initialization operation, where no preconditions are present [Bou93]3. This is done following the chemical semantics where conditions can only be stated on the local molecules involved in the rule

UBLCS-96-6 9

4 Specifying the dynamics of Z specifications Example To clarify this interpretation let us consider again the Lift system.The initialization operation (

Init System) is mapped on a chemical rule having no conditionsand no pretuples and as posttuples the following solution:

(position; fl; 1); (direction; DIRECTION ; up); (state; STATE ; stopped); (door; DOOR; open)

The state schema instance obtained after the application of the operation is the same solutionpresented above.

The rule associated to the operation schema Make Requests has the following posttuple (nopremises):

(requests; ff(REQUEST TYPE \Theta  fl); (r?; f ?)) The rule corresponding to the operation Move Up Up (Move Down Up is similar) has thefollowing condition

f ? pos, as premises:

(door; DOOR; closed); (requests; ff(REQUEST TYPE \Theta  fl); (up request; f )); (position; fl; pos); (direction; DIRECTION ; up)

and as consequences:

(direction; DIRECTION ; up)); (position; fl; pos + 1)); (state; STATE ; moving); (door; DOOR; closed); (requests; ff(REQUEST TYPE \Theta  fl); (up request; f ))

Rules which do not act on the same molecules can react simultaneously: hence, following ourinterpretation, enabled operation schemas which do not modify the same variables can react in

parallel.We remark that both sets and bags can be decomposed in several molecules thus increasing potential concurrency. For example, the set requests is decomposed in many molecules, one foreach request: in this way it is possible to have concurrency among different applications of the operation Make Requests. 4.2 An abstract execution model and its logic We define now an execution model, namely a way of abstractly executing a Z specification docu-ment, and a Unity-like logic to reason on properties exhibited by such a model.

The execution model is defined on the semantics just described; it represents the unfolding ofthe application of the rules of the operational semantics. For every state schema s an abstract execution tree can be constructed in the following way:

ffl the root node is void; ffl the first operation applied is the initialization operation having no preconditions; ffl from every node there can be several different applicable operation sets (chosen in the setof all the enabled operations on that node) depending on the non determinism of the choice

of the operations being in conflict. Each branch corresponds to the application of a groupof enabled operations that could be applied without conflicts, as dictated by the CHAM model [BB92].Figure 2 illustrates the construction of the execution model. In order to allow the specification of the Unity-like logic constructs using Z as meta-languagewe introduce the specification of the execution tree:

TREE ::= Void tree

j fork`PAIR \Theta  seq TREE '

where

PAIR == SCHEMA INSTANCE \Theta  seq ff SCHEMA OP

UBLCS-96-6 10

4 Specifying the dynamics of Z specifications Init_Instance ... .....

..

....

... ... ...

...State State

State State State

State

Void

Figure 2. Execution model Function Exec maps every state schema on an execution tree with specific properties (we omitthe Z specification of the function); the chemical interpretation imposes that for every node label (s; seq), where s is an instance and seq is a sequence of operations sets:

ffl all operations in the sets belonging to the sequence seq must be enabled on s; ffl all operations in the sets belonging to the sequence seq must act on the state schema ofwhich

s is instance; ffl each set member of the sequence seq must contain operations that can concur (that is withoutconflicts);

ffl for every s0 in the pair (s0; seq0), label of one of the children of the node labeled (s; seq), theremust hold the postconditions of all the operations in the operations set applied to reach that

node (sequence structure help to keep link between nodes and operations set). 4.3 A logic for expressing dynamic properties Properties have a chemical interpretation as well, so that we can analyze their truth on theexecution model.

In order to be able to reason on dynamic properties, like deadlocks and starvation, we borrowa few constructs from the Unity logic: Unless p unless q says that whenever p is true during the execution, surely q will become true or pcontinue to be hold. In particular, on the tree: if

p is true on some nodes then on their children qwill be true or still p holds.Stable

stable p is an alias for p unless false, that is when p become true it will hold forever.On the tree: if

p is true on a node it will remain true for all the subtree of that node.Invariant

invariant p says that p is true forever.That is, for every node of the execution tree

p is valid.Ensures

The meaning of p ensures q is that when p become true than eventually q will hold and beforethat moment

p is still valid.That is, if p is true on a node q will eventually hold on a node in all its subtree and before thatmoment p will be valid on all the nodes visited.Leads to

p leads to q has quite the same meaning of p ensures q except for the fact that it does not ensurethat

p is valid until q become true; on the tree: if p is true on a node q will eventually hold on a

UBLCS-96-6 11

4 Specifying the dynamics of Z specifications node in all its subtree.The following axiomatic schema shows how we formalize the meaning of the logic constructs on the execution model. We report only the unless and ensures functions:

unless : PROPERTY \Theta  PROPERTY " B 8 p; q : PROPERTY ffl unless(p; q) = true ,

(8 e : TREE ; e1 : seq TREE ; schema : SCHEMA STATE ; set : seq ff SCHEMA OP; inst : SCHEMA INSTANCE j subtree(Exec(schema); e) = true ^ fork(inst; set; e1) = e ^ valid(inst; and(p; not(q)) = true ffl (8 e3 : seq TREE ; set0 : seq ff SCHEMA OP; inst0 : SCHEMA INSTANCE ; e2 : TREE j e2 in e1 ^ fork(inst0; set0; e3) = e2 ffl valid(inst0; or(p; q)) = true))

where function valid indicates when a property holds on an instance state: intuitively this isdone considering every property as a solution and analyzing the matching with the state solution

like what has been done for rules.

ensures : PROPERTY \Theta  PROPERTY " B 8 p; q : PROPERTY ffl ensures(p; q) = true ,

((unless(p; q) = true) ^ (8 e : TREE ; e1 : seq TREE ; schema : SCHEMA STATE ; set : seq ff SCHEMA OP; inst : SCHEMA INSTANCE j subtree(Exec(schema); e) = true ^ fork(inst; set; e1) = e ^ valid(inst; and(p; not(q)) = true ffl (9 e3 : seq TREE ; set0 : seq ff SCHEMA OP; inst

0 : SCHEMA INSTANCE ; e2 : TREE j

subtree(e2; e) ^ fork(inst0; set0; e3) = e2 ffl valid(inst0; q)) = true))

The formalization for ensures derives from unless: in fact, p ensures q if p unless q and abranch exists which from a state where

p is valid (and not q) leads to a state where q holds.Having described the meaning of these logic predicates on the operational model, we can define and reson on dynamic properties on the abstract concurrent interpretation of Z specifications.

Example We specify and verify dynamic requirements with the help of the new constructs. Wehave already defined three properties on the Lift specification in Sect.3: now we analyze the specification trying to prove them.

Theorem 1: Invariant door = open ) state = stoppedProof: To prove an invariant property we prove that the property holds after the initialization

and that it is stable.The first condition is true: in fact, the

Init Lift System operation assigns the value open to the door variable and stopped to the lift state. Stable(p) is p Unless false: that is, for every operationsset applicable to a state where

p ^ : false = p ^ true = p is valid, the next state in the executionwill satisfy p . false = p.In our particular case, consider

p as the property door = open ) state = stopped; given a statewhere p holds, all the operations are enabled, in fact p is also door = closed . state = stopped.The operation

Make Requests does not modify the lift state while other specification operationschange it accordingly to the invariant. Moreover, operations sets to be executed can contain one

operation only acting on the lift system (all the operations on the lift need to modify the samemolecules) plus several

Make Requests. Then we can conclude that the invariant holds.

UBLCS-96-6 12

5 Animating a Z specification Theorem 2: (t; f ) 2 requests ^ f = position ^ door = closed ensures door = openProof: If

p ensures q (where p is (t; f ) 2 requests ^ f = position ^ door = closed and q is door = open) must be valid, first p unless q has to hold (see the formalization). That means that forevery enabled operations set on the solution containing molecules

(requests; ff(REQUEST TYPE \Theta  fl); (t; f )), (position; fl; pos) and (door; DOOR; closed), the application leads to a state wheremolecule

(door; DOOR; open) is present or the previous molecule is still in the solution (thisis the unless formalization of our concurrent execution model).

Considering our Z specification, we notice that the only enabled operations on an instance statecontaining those molecules are

Make requests (that only adds new requests molecules withoutmodifying the lift state) and Open Door that exactly open the lift door. Hence, p unless q holds.To prove p ensures q is now necessary to ensure that, given a state where p ^ : q holds existsan enabled operations set applicable, which leads to a state in which

q holds. In our specificationsuch a set is composed of operation Open Door and some (or none) Make Requests.This completes the proof.

Theorem 3: (r; f ) 2 requests ^ r ? position ^ direction = up ^ state = moving ^ door = closed leads to position = rProof: in order to prove a

p leads to q property we must ensure that at least one chain ofoperations sets does exist starting from a state containing the molecules

(requests; ff(REQUEST TYPE \Theta  fl); (r; f )), (direction; ff DIRECTION ; up), (position; fl; pos), (with r ? pos), (state; ff STATE ; moving) and (door; ff DOOR; closed), leadingto a state containing

(position; fl; r).The operations sets in the chain are composed of the operation

Make Requests and Move Up Up,which continuously move the lift up until requests are present above the lift position.

5 Animating a Z specification A formal requirements document provides a precise and rigorous description of the system beingdeveloped. Its aim is to define abstract properties of the system, describing what the system has

to do and not how to do it [HJ89]. Z is not executable because it allows to declare not computableentities, like infinite sets or non computable functions, and to express properties and operations on them.However, it is often desirable to have a prototype of the system which can be tested and whose dynamic properties can be directly inspected by either the specifier or even the customer.The technique of animation has been introduced in order to overcome the difficulty of obtaining a prototype from a non executable specification language like Z. Several approaches have beenused to animate a Z specification, using different methods and languages; a short review can be found in [SCT96]. All the proposed solutions have to balance declarativeness versus efficiency inthe sense that we want not only an executable form of a very high level specification, but also a reasonably efficient execution to test the specification [BB94].We stress the fact that Z has on purpose no executable operational semantics [HJ89]. However, there is a problem: these languages are intended to make simple the proving of importantproperties of the software system specification being studied, but they cannot help in establishing a very important property from a practical point of view: executability of the specification [Fuc92].Moreover, software developers wanting to experiment with intermediate specifications to gain feedback from the client are deprived from using the computer to test the current version.The semantics we gave in Sect.4 is useful not only to reason on Z documents, but also to animate them. Such a semantics is chemical and intrinsically parallel, so we expect to have aparallel/distributed animation. In fact, we describe now a method for the distributed animation of specification documents written in Z by translating them into programs written in thecoordination language Shared Prolog [CG96], an extension of Prolog with support for explicit parallelism whose semantics is also based on the chemical model [Cia91].Our approach to parallel animation consists of refining the original specification to obtain a more procedural version directly executable by generate-and-test clauses and queries. We define UBLCS-96-6 13

5 Animating a Z specification a subset of Z in which specifications must be refined before the animation process is carriedon. The translation from such a refined specification to the animation language is automatically performed by a source-to-source translator which produces a correct distributed program inShared Prolog. The code obtained is finally compiled by the SP compiler [CG94] and executed over a network of workstations.Unlike other animators (e.g. Zans [Jia95]) that simply offer a way of executing sequentially and step by step single operations, our animator generates Shared Prolog code that is an executableform of the Z specification able to generate a parallel trace including several (potentially infinite) operations.

5.1 The animation language The animation language we target is Shared Prolog, that is based on the combination of the shareddataspace coordination model (as in Linda) with logic programming computing (as in Prolog)

[CG96].A program in Shared Prolog consists of a set of modules called theories, an initial goal and an initial coordination medium called tuple space or blackboard. The blackboard is a multiset oflogical tuples (Prolog atoms). The initial content of the blackboard is defined by a special goal:

tuple_space{tuple-1, ... ,tuple-n}. Another special goal defines some agents which share the tuple space (we also call agents"active tuples", since they are part of the tuple space):

initial_goal(agent-1 '||' .. '||' agent-n. An agent represents a process executing a theory and accessing the tuple space for read-ing/consuming/producing tuples. A theory is a Prolog program extended with mechanisms for

coordination through the tuple space.Each theory is composed of a set of patterns and a knowledge base. Syntactically a theory looks as follows:

agent theory_name (V_1,..,V_n)

eval

pattern_1 #

... #

pattern_k with knowledge base

The theory name is a functor with zero or more arguments Vi which are logic variables scopingover all the patterns.

A pattern has the following form:

{in_guard},read_guard

---> body out_set,

fail failure_set

The in guard and the read guard are evaluated trying to unify a multiset of tuples in theblackboard with those contained in the guard. The body of a pattern contains predicates defined

in the knowledge base of the theory. Semantically, each pattern consists of two components namedpreactivation and postactivation. The former defines an activation condition consisting of reading and/or deleting some tuples from the blackboard. The latter consists of a Prolog goal (body) andtwo multisets of tuples: one to be added to the blackboard in case of successful evaluation of the goal (out set), and the other to be added in case of body failure (failure set).Initially, every pattern of a theory is examined to check the satisfiability of its own guard. If a guard is satisfied, the corresponding body is evaluated and tuples are added to the blackboard.If several patterns satisfy their preactivation, one is nondeterministically chosen and executed.

UBLCS-96-6 14

5 Animating a Z specification 5.2 Animating a Z specification with SP According to the specification style described in Sect.4, a Z specification document is composed ofstate schemas which contain predicates on the abstract state of the system, and operation schemas

which contain predicates describing how the state of the system may evolve. Operation schemasconsist of a set of preconditions which specify the set of valid states of the system to which it is possible to apply such an operation and a set of postconditions which define the set of states thatcan be reached after the application of the operation itself.

An operation is enabled if the current state of the system satisfies its preconditions; two (ormore) operations are concurrent if they are enabled at the same time. This implies that in the animation, several operations can be executed at the same time. In fact, the animation of arequirements specification document using a concurrent language has the immediate effect of capturing and making observable the concurrent characteristics of the system being specified.In our case every Z schema corresponds to a pattern in a theory in the SP program obtained by translation of the specification. Theories correspond to complex operations built using schemaexpressions.

In order to simplify the translation we have restricted Z to a number of constructs (we call Zel- Z elementary - the resulting notation). In the following table is summed up what can be used in Zel:

Predefinite types fl; AEType constructors

ff; bag; seq; \Theta Operators on set 2; 62; [; "; ae; `Operators on multiset \Phi ; ]; !Operators and functions on sequences in; O/; head; tail; front; lastArithmetic operators + , - , * ,

div , modRelational operators =; 6=; ?; !; *; ^Logical operators : ; ^Quantifiers 9Schema connectives .; ^; ); o/; ??Variable decorations ! , ? ,

0

The restrictions we have introduced concern types and use of variables, form of predicates,and usability of some quantifiers.

5.2.1 Types Types can be defined in Zel as follows:

ffl predefinite type, as fl e AE; ffl given set; ffl structured type, defined by enumerating elements; ffl applying type constructors as ff,bag,seq,\Theta ; ffl schema type.

5.2.2 Variables Variables in the declarative part of a schema must be defined as ff, bag or seq of another type X,because they are mapped into SP tuples, as we will see later. These restrictions do not apply if

a variable is inside the scope of an existential or universal quantifier in the predicative part of aschema.

Special attention must be paid to i/o variables. If the type of an input(output) variable isdefined as

ff X , the corresponding predicates must be translated using another variable of type Xexistentially quantified and whose singleton set must be equal to the original variable.

UBLCS-96-6 15

5 Animating a Z specification 5.2.3 Predicates In our approach only a subset of Z predicates can be used in specifications, since not all thepredicates are easy to animate. In the predicative part of a schema, it is possible to use only

^ aslogical operator, while : can be used in conjunction with membership tests.The order of the predicates is important and influences the SP program obtained from the

animation. One must pay attention to define predicates without unbound variables, so that thecorresponding SP program does not evaluate non ground terms. However, properties can be defined using non animatable predicates and the syntactical restrictions are not applied; onlyunder these circumstances other logical operators (e.g.

.) or the universal quantifier are allowed.Although these predicates are type checked, they produce no effect on the resulting animation.

5.3 From Zel to SP Once a Zel specification document has been obtained (by manual refinement of the originalZ specification) the animation process continues using a translator tool which automatically

produces a SP program. We now describe the ideas we used to build the translator.Each simple schema not defined by a schema calculus expression in the Zel document is transformed in a SP pattern; instead, a schema defined by a schema calculus expression istranslated into a theory containing the patterns corresponding to the simple schemas which are operands in the expression.To each variable defined in the predicative part of a Zel schema corresponds a unique SP tuple in the blackboard, obtained concatenating the name of the variable and of the schema in which itis defined. Input variables are removed from the blackboard, while output variables are added. For each schema, the system tries to determine a couple of animatable predicates in the list ofprecondition and postconditions, and the corresponding action is added to the pattern.

Example Suppose that in a precondition we have a set membership predicate, and in the post-condition we update the the set removing the tested element.

precondition v 2 setpostcondition set

0

= set n fVg

pattern fset(v)g ! ..

In the SP program this is equivalent to including a tuple in the in-guard of the correspondingpattern, with the meaning that it will be removed from the blackboard.

5.4 Querying the animation The SP program obtained from the transformation process has to be initialized before it can beexecuted. The initial state of the blackboard and the initial goal in fact cannot be obtained by

automatic translation of the specification, but must be defined in the query.In the version we use, SP programs are static: it is not possible to activate agents during the execution, they must be all defined in the initial goal. Moreover, tuples representing input datafor the animation must be added to the tuple space in the initial blackboard. Once the initial goal has been defined and the tuple space has been opportunely modified, the SP program is passedto the Shared Prolog compiler producing the executable code corresponding to the requested animation. This code runs on a network of workstations.The following diagram visualizes the animation process for a given specification:

UBLCS-96-6 16

6 Animating the Lift System SpecificationZel SPProgram ExecutableCode

Query 6 Animating the Lift System We describe now the animation of the specification of the lift system introduced in Sect.3. The firststep consists of refining the Z document. This amounts to refining and simplifying Z schemas

into Zel syntax.For instance, the following schemas describe the operation of moving the lift up, provided that there is at least one pending request above its current position either when the lift is goingup or when there are no more requests going down. Note how few changes have been made wrt the original version given in Sect.3: they only concern variables defined as ff sometype and i/ovariables.

Move Up Up \Delta LiftSystem

9 tf : REQUESTTYPE \Theta  fl; t : REQUESTTYPE ; f ; p1; p2 : fl; d : DOOR; c : DIRECTION ffl

(tf 2 requests ^ tf = (t; f ) ^ p1 2 position ^ f ? p1 ^ p2 = p1 + 1 ^ d = closed ^ d 2 door ^ c = up ^ c 2 direction ^ position0 = position n fp1g [ fp2g ^ direction0 = fupg ^ state0 = fmovingg ^ door0 = fclosedg)

Move Down Up \Delta LiftSystem

9 tf : REQUESTTYPE \Theta  fl; t : REQUESTTYPE ; f ; p1; p2 : fl; d : DOOR; c : DIRECTION ffl

(tf 2 requests ^ tf = (t; f ) ^ p1 2 position ^ f ? p1 ^ p2 = p1 + 1 ^ d = closed ^ d 2 door ^ c = down ^ c 2 direction ^ : (9 ug : REQUESTTYPE \Theta  fl; u : REQUESTTYPE ; g : fl ffl

(ug 2 requests ^ ug = (u; g) ^ g ^ p1)) ^ position0 = position n fp1g [ fp2g ^ direction0 = fupg ^ state0 = fmovingg ^ door0 = fclosedg)

The next step is the automatic translation of the specification in Shared Prolog. Here is thecode obtained by translating the schema

Move Up Up above reported.

UBLCS-96-6 17

6 Animating the Lift System {moveupup}, {position__liftsystem(P1)}, requests__liftsystem(TF), TF=(T,F), F>P1, P2 is P1 + 1, D=closed, door__liftsystem(D), C=up, direction__liftsystem(C), {findall(direction__liftsystem(_V3),_V4)}, {findall(state__liftsystem(_V5),_V6)}, {findall(door__liftsystem(_V7),_V8)} ->

{position__liftsystem(P2), direction__liftsystem(up),

state__liftsystem(moving), door__liftsystem(closed)}

The initial tuple space is obtained from the InitSystem Lift schema defined in the specificationdocument. It can be modified to satisfy a particular query to be animated. In the following example, we put into the tuple space a set of tuples representing a sequenceof service requests for the lift, and an initial condition for the lift.

tuple_space{position__liftsystem(1),direction__liftsystem(up),

state__liftsystem(stopped),door__liftsystem(open), r((upRequest,3)),r((upRequest,1)),r((upRequest,4))}.

Moreover, at least one agent has to be activated by the initial goal:

initial_goal (op_liftsystem). The SP program is then compiled and executed. Trace (a) below shows the report of ananimation of the system for the above sequence of service requests, including the final state of

the lift.

req upRequest,3 req upRequest,1 close[] up from 1 to 2 up from 2 to 3 open 3 req upRequest,4 close[] up from 3 to 4 open 4 final set:[(upRequest,4)] final position: floor 4 door: open

trace(a)

req upRequest,3 up from 1 to 2 up from 2 to 3 open 3 req upRequest,4 close[] up from 3 to 4 open 4 req upRequest,5 up from 4 to 5 open 5 close[] down from 5 to 4 open 4 final set:[(upRequest,4)] final position: floor 4 door: open

trace(b)

A trace helps the specifier to debug a specification. He should aim at checking aspects of thesystem that have not been fully explored or to correct an improper behavior due to mistakes in the specification.For instance, trace b) shows the animation report if we "forget" to include in the

Move Upschemas the test concerning the shutting of lift door. The trace shows that a lift can move to a

new floor to satisfy a request without closing its door; moreover, since requests are deleted in the Close Door schema, request for floor 4 remains among the pending requests list and it is servicedtwice.

Testing a specification can be carried on giving in input different test cases that are instances ofa particular functional requirement and observing the resulting animation. An unsuccessful case shows that the functional requirements tested is not valid, but only if all instances of a functionalrequirement are tested satisfiability is demonstrated [Kem85]

The main advantages of the animation are in terms of accelerating the validation of the UBLCS-96-6 18

7 Refining the animation specification with respect to the user requirements and increasing the degree of trust the specifiercan have in the system being built.

7 Refining the animation Since the process of obtaining an animation is automatic, it is possible to rapidly build a prototypeof the system even if the original specification is incrementally modified in order to test different

or new features. The feedback coming from the execution of the animation can be used to improveor emend the original specification document.

For instance, we can refine our example to make the lift system more realistic increasingthe number of lifts and specifying a scheduling policy for user requests. This can be easily accomplished parameterizing opportunely the operations and the state of the original lift system.The modified schema looks as:

LiftSystem position : ff(LIFT \Theta  fl) direction : ff(LIFT \Theta  DIRECTION ) state : ff(LIFT \Theta  STATE ) door : ff(LIFT \Theta  DOOR) requests : ff(LIFT \Theta  REQUESTTYPE \Theta  fl) Lifts : ff LIFT

where LIFT ::= a1 j a2 j a3 defines the available lifts.The following schema refines the corresponding one presented in the preceding section.

Move Up Up \Delta LiftSystem

9 tf : LIFT \Theta  REQUESTTYPE \Theta  fl; t : REQUESTTYPE ; e : LIFT ; f ; p1; p2 : fl; d : DOOR; c1; c2 : DIRECTION ; s1; s2 : STATE ffl (tf 2 requests ^ e 2 Lifts ^ tf = (e; t; f ) ^ (e; p1) 2 position ^ f ? p1 ^ p2 = p1 + 1 ^ (e; d) 2 door ^ d = closed ^ (e; c1) 2 direction ^ c2 = up ^ (e; s1) 2 state ^ s2 = moving ^ position0 = position n f(e; p1)g [ f(e; p2)g ^ state0 = state n f(e; s1)g [ f(e; s2)g ^ direction0 = direction n f(e; c1)g [ f(e; c2)g)

The operation Move Up Up is now enabled when one of the active lifts has to serve a request ata floor above its current position; state, direction, and position of the moving lift are consequently updated. User requests are scheduled by a controller which assigns each pending request to thelift nearest to the requested floor.

UBLCS-96-6 19

7 Refining the animation Controller \Delta LiftSystem r? : ff(REQUESTTYPE \Theta  fl)

9 s : REQUESTTYPE \Theta  fl; r1 : LIFT \Theta  REQUESTTYPE \Theta  fl; t : REQUESTTYPE ; e1 : LIFT ; a; f ; a1; p1 : fl ffl (fsg = r? ^ s = (t; f ) ^ (e1; p1) 2 position ^ a = p1 \Gamma  f ^ a1 = a \Lambda  a ^ : (9 e2 : LIFT ; b; b1; p2 : fl ffl ((e2; p2) 2 position ^ b = p2 \Gamma  f ^ b1 = b \Lambda  b ^ b1 ! a1)) ^ r1 = (e1; t; f ) ^ requests0 = requests [ fr1g)

A change of scheduling policy of requests involves the redefinition of the above schema; theconsequences over the whole system can be inspected through the execution trace. Concurrency of operations of different lifts can be appreciated since concurrent enabled operations are concur-rently executed. What follows is the trace of the animation of a lift system composed of three lifts and a scheduler assigning requests as specified above. The final state of the system with a set ofpending requests is also showed. Controller Lift a1 Lift a2 Lift a3 req upRequest,1 assign a1

lift a1 open 1 req upRequest,8 assign a1

lift a1 close lift a1 up from 1 to 2 lift a1 up from 2 to 3 lift a1 up from 3 to 4 lift a1 up from 4 to 5 lift a1 up from 5 to 6 lift a1 up from 6 to 7 lift a1 up from 7 to 8 lift a1 open 8 req upRequest,4 assign a2

lift a2 up from 1 to 2 lift a2 up from 2 to 3 lift a2 up from 3 to 4 req upRequest,3 assign a2 req upRequest,5 assign a2 req upRequest,3 assign a2 req upRequest,1 assign a3 req upRequest,6 assign a1 req upRequest,4 assign a2 req upRequest,3 assign a2 req upRequest,1 assign a3 req upRequest,2 assign a3 req upRequest,8 assign a1 req upRequest,4 assign a2 req upRequest,3 assign a2

lift a1 close

lift a2 open 4 lift a2 close

lift a3 open 1 lift a3 close lift a1 open 8 lift a1 close lift a1 down from 8 to 7

lift a2 open 4 lift a2 close

lift a3 open 1 lift a3 close lift a3 up from 1 to 2 lift a2 open 4 lift a2 close

lift a3 open 2 lift a1 down from 7 to 6 lift a1 open 6

lift a2 up from 4 to 5 lift a2 open 5 lift a2 close lift a2 down from 5 to 4 lift a2 down from 4 to 3 lift a2 open 3

UBLCS-96-6 20

8 Conclusions and future works requests [(a2,upRequest,3),(a2,upRequest,3),(a1,upRequest,6),

(a2,upRequest,3),(a3,upRequest,2),(a2,upRequest,3)] position [(a3,2),(a1,6),(a2,3)] door [(a3,open),(a1,open),(a2,open)] direction [(a3,up),(a1,down),(a2,down)] state [(a3,stopped),(a1,stopped),(a2,stopped)]

The trace given above shows that the controller correctly assigns requests to the lifts whichconcurrently move from floor to floor serving the formerly scheduled requests. Note how the arrival of a request to the floor where a lift has already stopped causes the reopening of the doors.This and other strange behaviors, if found, can be corrected furtherly refining the specification.

8 Conclusions and future works When formal requirements specification is the first phase in a software development process basedon formal methods, the possibility of analyzing and testing relevant properties of requirements

(including the implementability/executability property) early in the process avoids to carry costlymistakes over the next phases.

We have introduced two methods for the analysis of specification dynamics: the first one ismore abstract, and it is able to deal with global behavioral components, whereas the second is more concrete, and able to produce a high level prototype. The prototype itself can be used tostudy the specification behavior, producing test cases which can be used in subsequent phases.

The main novelties of our approach are the introduction of a chemical operational semanticsfor Z, which offers the formal basis to analyze dynamic properties of reactive systems, and the automatic development of a concurrent animation using a prototyping language able to highlightconcurrent behaviors.

Our work can be closely compared with the one exposed in the classic paper [Kem85]. Themain difference is that our method aims clearly at the requirements specification document, whereas Kemmerer was apparently more interested in design. We believe it is important to clearlydistinguish requirements specification from design specification [CCP95], and to introduce and study methods and tools for the analysis, testing, and verification of the requirements specificationdocument.

Some formal approaches integrate Z with other notations; for instance, Benjamin [Ben89]integrates Z schemas with CSP notation. CSP is used to specify abstract operations, while Z is used for detailing some design features of abstract state and data. The integration is very lowlevel and not formally specified. In [He95] Petri Nets are used to formalize control flows, causal relations, and dynamic behavior of systems statically specified using Z; there is no formalizationof the interaction between the two notations.

[Eva94b] offers a more formal model of integration of Z with Petri Nets: Petri Nets are mappedon Z specifications so that graphical representation given by Petri Nets can be used to visualize Z specified systems, yet we think a visualization cannot replace formal semantics.In [RAO92] a formalism based on temporal logic is used to integrate Z schemas with dynamic properties. The use of temporal logic offers good starting points to the study of the dynamics ofZ specifications, however the integration is not supported by a formal semantics. In this sense something more formal has been done for Object-Z [CDD+89]: a sequential execution model isintroduced, defining a notion of abstract trace as a sequence of pairs (states and operations), and using some temporal logic operators (3, 2, flflfl) to reason on such a model.Following a similar approach, the temporal logic of actions (TLA) has been used to give formal semantics to dynamics in Z specifications [BL95]. The suggested model is quite complexand specifications are difficult to analyze because concurrency is interpreted as conjunction of operations. A simpler approach has been suggested by Evans in [Eva94a]. He uses a Unity likelogic [MM88] to formalize properties on the behavior of systems; an interleaving model with atomic operation interpretation is given but not formalized. UBLCS-96-6 21

REFERENCES Our approach shows how the simplicity and conciseness of Unity logic constructs fit quitewell with the operational semantics based on CHAM. We have been using the notations and tools described in this paper in an undergraduatecourse on requirements engineering. Several student projects have been completed, and now we are analyzing such an experience to evaluate the overall approach. The major shortcomingsour users have found concern the compiler tool: it lacks support for incremental debugging. Another aspect we are investigating is the formal relationship between the operational semanticsand the original declarative semantics of Z. We are studying correctness and completeness of our semantics with respect to the original one.

Acknowledgments. Partial support for this work was provided by the Commission of Euro-pean Union under ESPRIT Programme Basic Research Project 9102 (COORDINATION), and by the Italian MURST 40%- Progetto "Ingegneria del Software".

References

[BB92] G. Berry and G. Boudol. The Chemical Abstract Machine. Theoretical Computer Science, 96:217-248, 1992.

[BB94] P. Breuer and J. Bowen. Towards Correct Executable Semantics for Z. In J. Bowen and J. Hall,editors, Proc. 8th Z Users Workshop (ZUM94), Workshops in Computing, pages 185-212, Cambridge, 1994. Springer-Verlag, Berlin. [Ben89] M. Benjamin. A Message Passing System. An example of combining Z and CSP. In J. Nicholls,

editor, Proc. 4th Z Users Workshop (ZUM89), Workshops in Computing, pages 221-228, Oxford,1989. Springer-Verlag, Berlin.

[BG94] J. Bowen and M. Gordon. Z and HOL. In J. Bowen and J. Hall, editors, Proc. 8th Z Users Workshop(ZUM94), Workshops in Computing, pages 141-167, Cambridge, 1994. Springer-Verlag, Berlin. [BG95] J. Bowen and M. Gordon. A Shallow Embedding of Z in HOL. Information and SoftwareTechnology, 37(5-6):269-276, May-June 1995. [BKKT95] A. Bloesch, E. Kazmierczak, P. Kearney, and O. Traynor. Cogito: Methodology and System forFormal Software Development. Int. Journal on Software Engineering and Knowledge Engineering,

5(4):599-618, 1995. [BL95] P. Baumann and K. Lermer. A Framework for the Specification of Reactive and Concurrent

Systems in Z. In P. Thiagarajan, editor, Proc. 15th Conference on Foundation of Software Technologyand Theoretical Computer Science, volume 1026 of Lecture Notes in Computer Science, pages 62-79,

Bangalore, India, 1995. Springer-Verlag, Berlin. [BN92] S. Brien and J. Nicholls. Z Base Standard, November 1992. Programming Research Group. [Bou93] G. Boudol. Some Chemical Abstract Machines. In J. deBakker, W. deRoever, and G. Rozenberg,editors, A Decade of Concurrency, volume 803 of Lecture Notes in Computer Science, pages 92-123.

Springer-Verlag, Berlin, 1993. [BSC94] R. Barden, S. Stepney, and D. Cooper. Z in Practice. Prentice-Hall, 1994. [CCP95] P. Ciaccia, P. Ciancarini, and W. Penzo. A Formal Approach to Software Design: The Clepsydra

Methodology. In J. Bowen and M. Hinchey, editors, Proc. 9th Int. Conf. on the Z Formal SpecificationNotation (ZUM95), number 967 in Lecture Notes in Computer Science, pages 5-24, Limerick,

Ireland, September 1995. Springer-Verlag, Berlin. [CDD+89] D. Carrington, D. Duke, R. Duke, P. King, G. Rose, and G. Smith. Object-Z: an Object-OrientedExtension to Z. In Formal Description Techniques (FORTE 89), pages 281-296. North-Holland,

1989. [CG94] P. Ciancarini and M. Gaspari. Parallel Symbolic Computing with the Shared Dataspace Coordi-nation Model. In K. DeBosschere, JM. Jacquet, and A. Brogi, editors, Workshop on Process-based

Parallel Logic Programming, pages 11-38, S.Margherita Ligure, Italy, June 1994. [CG96] P. Ciancarini and M. Gaspari. Rule Based Coordination of Logic Programs. Computer Languages,(to appear), 1996.

[Cia91] P. Ciancarini. Parallel Logic Programming Using the Linda Model of Computation. In JP. Banatreand D. LeMetayer, editors, Research Directions in High-Level Parallel Programming Languages,

volume 574 of Lecture Notes in Computer Science, pages 110-125, Mont Saint-Michel, France, June 1991. Springer-Verlag, Berlin.

UBLCS-96-6 22

REFERENCES [CWB94] J. Cuellar, I. Wildgruber, and D. Barnard. Combining the design of industrial systems witheffective verification techniques. In FME'94: Industrial Benefit of Formal Methods, volume 873 of

Lecture Notes in Computer Science, pages 639-658, Barcelona, Spain, 1994. Springer-Verlag, Berlin.[Dil90] A. Diller. Z: An Introduction to Formal Methods. Wiley, New York, 1990. [DJ96] C. Damon and D. Jackson. Efficient Search as a Means of Executing Specifications. In Proc.TACAS '96

, volume (to appear) of Lecture Notes in Computer Science. Springer-Verlag, Berlin,March 1996.

[DKC89] A. Dick, P. Krause, and J. Cozens. Computer aided transformation of Z into Prolog. In

J. Nicholls, editor, Proc. 4th Z Users Workshop, Workshops in Computing, pages 71-85, Oxford,1989. Springer-Verlag, Berlin.

[Eva94a] A. Evans. Specifying and Verifying Concurrent Systems Using Z. In M. Bertran, T. Denvir, andM. Naftalin, editors, Proc. FME'94 Industrial Benefits of Formal Methods, volume 873 of Lecture

Notes in Computer Science, pages 366-380. Springer-Verlag, Berlin, 1994.[Eva94b] A. Evans. Visualizing Concurrent Z Specifications. In J. Bowen and J. Hall, editors, Proc. 8th Z Users Workshop (ZUM94), Workshops in Computing, pages 269-281, Cambridge, 1994. Springer-Verlag, Berlin.[Fuc92] N. Fuchs. Specifications are (preferably) executable. IEE Software Engineering Journal, 7(5):323-

334, September 1992.[GGMM87] F. Garzotto, C. Ghezzi, D. Mandrioli, and A. Morzenti. On the specification of real-time systems using logic programming. In Proc. 1st European Software Eng. Conf. (ESEC), volume 289 of LectureNotes in Computer Science

, pages 180-190. Springer-Verlag, Berlin, 1987.[GLW90] P. Gardiner, P. Lupton, and J. Woodcock. A simpler semantics for Z. In J. Nicholls, editor, Proc.

5th Z Users Workshop, Workshops in Computing, pages 3-11. Springer-Verlag, Berlin, 1990. [Hay93] I. Hayes. Specification Case Studies. Prentice-Hall, 2 edition, 1993.[He95] X. He. PZ Nets: A Formal Method Integrating Petri Nets with Z. In Proc. 7th Int. Conf. on Software

Engineering and Knowledge Engineering, pages 173-180, Rockville, Maryland, 1995. KnowledgeSystems Institute. [HJ89] I. Hayes and C. Jones. Specifications are not (necessarily) executable. IEE Software EngineeringJournal, 4(6):330-338, November 1989. [IW95] P. Inverardi and A. Wolf. Formal Specification and Analysis of Software Architectures Using

the Chemical Abstract Machine Model. IEEE Transactions on Software Engineering, 21(4):373-386,April 1995.

[Jac94] D. Jackson. Abstract Model Checking of Infinite Specifications. In M. Naftalin, T. Denvir, andM. Bertran, editors, Proc. 2nd Int. Symp. of Formal Methods Europe (FME), volume 873 of Lecture

Notes in Computer Science, pages 519-531, Barcelona, Spain, October 1994. Springer-Verlag, Berlin.[Jia94] Xiaoping Jia. ZTC: a type checker for Z. User's guide, 1994. Institute of Software Engeneering.

[Jia95] Xiaoping Jia. An Approach to Animating Z Specifications, 1995. Institute of Software Engeneering.[Kem85] R. Kemmerer. Testing Formal Specifications to Detect Design Errors. IEEE Transactions on

Software Engineering, 11(1):32-43, January 1985.[MM88] K. ManiChandy and J. Misra. Parallel Programming Design. Addison-Wesley, 1988. [RAO92] D. Richardson, S. Aha, and T. O'Malley. Specification-based Test Oracles for Reactive Systems.In Proc. 14th IEEE Int. Conf. on Software Engineering, pages 105-118, Melbourne, Australia, 1992.

[Saa89] M. Saaltnik. Z and Eves. In J. Nicholls, editor, Proc. Z User Workshop, Workshops in Computing,

pages 223-242, Oxford, UK, 1989. Springer-Verlag, Berlin.[SCT96] L. Sterling, P. Ciancarini, and T. Turnidge. On the Animation of Not Executable Specifications

by Prolog. Int. Journal on Software Engineering and Knowledge Engineering, 6(1):(to appear), 1996.[Spi88a] J. Spivey. The f

UZZ Manual, 1988.[Spi88b] J. Spivey. Understanding Z. Cambridge Tracts in Theoretical Computer Science. Cambridge

University Press, 1988.[Spi92] J. Spivey. The Z Notation. A Reference Manual. Prentice-Hall, 2 edition, 1992. [vSV91] K. vanHee, L. Somers, and Voorhoeve. Z and High Level Petri Nets. In S. Prehn and W. Toetenel,

editors, Proc. VDM 91: Formal Software Development Methods, volume 551, pages 204-219.Springer-Verlag, Berlin, October 1991.

UBLCS-96-6 23