Translator from CSP-Z to CSPM notation

A Java translator from CSP-Z to CSPM notation

Adalberto Farias, Alexandre Mota and Augusto Sampaio
Federal University of Pernambuco
Centre of Informathics
Pernambuco - Brazil

1. Introduction

This work deals with converting specifications written in CSP-Z to CSPM notation, used by FDR, and so allows the verification of desirable properties as deadlock-freedom. The adopted convertion strategy is detailed in Model-Checking CSPz: strategy, tool suport and industrial application. The translator was implemented in Java, at Laboratory of Formal Methods, at the Federal University of Pernambuco, Brazil and will be improved in later versions. We present one simple example CSP-Z specification and its CSPM notation generated by the tool. Mapping Z definitions to CSPM takes into account details that should be treated carefully. We present some of these limitations along the following topics.

2. Overview of CSPz

The language CSPz is a conservative extension of both CSP and Z preserving almost all syntactical and semantical aspects of each language. In a CSPz specifications the following aspects can be found:

CSP part - containing all channels, datatypes, processes and their behaviour in terms of synchronisation between them. There is only a little difference in CSPz channel daclarations that will be explained later.
Z part - contains data structures and schemas that represent the state space of the system, the state initialization and operations with its pre and pos-conditions. For each CSP event there is an associated Z schema which defines the state changes and communication effects caused by the occurrence of the CSP event.

3. Syntax of CSPz

Specifications written in CSPz have two separated parts(as explained above). There is only a subtle difference between channels in CSP and CSPz, as showed below:

In CSP:

        channel a          -- channels without parameters 
        channel b:X.Y      -- channels with parameters

In CSPz:

        channel a : []              -- channels without parameters 
        channel b : [x:X;y:Y]       -- channels with parameters

where x is a simple variable and X is its type. a and b are the channel identifiers. The other terms are identical to CSP and Z languages. Two special schemas should be in the Z part of the specification: State and Init.

The tool translates the Z and the CSP parts to the corresponding CSPM processes, and generates a top level process which synchronises the two generated processes. By convention the control flow starts with the first event of the process named main (CSP part). The Z part is translated into a process which is written as an external choice of all the system events, where after one single event was performed, the process recursevely offers all events again. The process which represents the Z part also takes into account the state, initialization and operation schemas.

All CSPz processes are declareted in a spec/end_spec clause. A CSPz specification has the following structure:

spec MY_SYSTEM
	-- CSP part
	datatype and channels declarations
	CSP processes
	main process

Z-PART  
	-- Z part
	z-types(given sets and freetypes)
	state schema
	init schema
	others schemas

end_spec MY_SYSTEM

4. Example of a CSPz Specification

This specification is a simple example written CSPz . The corresponding CSPM notation was generated by the tool and is presented in what follows. It is a simple clock containing two events: ticktack and bird. The first event hapens each minute and when it is equal to 60 its value is reset to 0 and the bird event occurs. The source code is showed below.

spec Clock 
	channel ticktack:[] 
	channel bird:[msg:SOUND] 
	main = ticktack -> main [] bird!msg -> main 
 
Z-PART
	\begin{zed}
	 Values == \{ 0 \upto 60 \}
	\end{zed}

	\begin{syntax}
	 SOUND == Cookoo
	\end{syntax}

	\begin{schema}{State} 
	 Min : \nat 
	\end{schema} 
 
	\begin{schema}{Init} 
	 State' 
	\where 
	 Min'= 0 
	\end{schema} 
 
	\begin{schema}{comticktack} 
	 \Delta State 
	\where 
	 Min < 60 \\ 
	 Min'= Min + 1 
	\end{schema} 
 
	\begin{schema}{combird} 
	 \Delta State \\ 
	 msg!: SOUND 
	\where 
	 Min=60 \\ 
	 Min'= 0 \\
	 msg!= Cookoo
	\end{schema} 

end_spec Cookoo

5. Strategy for the Conversion to CSPM

The key points to converting a CSP-Z specification into a CSPM specification are:

Schemas representing operations should perform actions over system data structures(if required), but not the CSP part.
CSP processes are represented by the main process
All schemas are converted to CSP processes incorporating pre and pos conditions.
Processes representing schemas are combined to form the Z process which is an external choice of all the events
Another process, maned Z_CSP takes into account the Z process and the system initialization aspects.
Finally all processes are declarated locally in a let clause where its within part is a generalized parallel composition between main and Z_CSP processes.

6. Example of Translation into CSPM

Here we present the CSPM description generated from the CSP-Z specification od the Cookoo.

datatype SOUND = Cookoo 
channel ticktack 
channel bird : SOUND 
Clock = 
  let 
	
	-- The interface 
	Channels = {|ticktack,bird|} 
	lChannels = {} 
	Interface = union(Channels,lChannels)    

	-- The CSP part 
	main = ticktack -> main [] bird?msg -> main 

	-- The Z part 
	Values = {0..60}
	State = { Min | Min <- Values }
	Init = { Min' | Min' <- Values , Min'==0 }
	com (Min,ticktack) = { Min' | Min' <- State, Min < 60,Min'==Min+1 }
	com (Min,bird.msg) = { Min' | Min' <- State, Min==60,Min'==0,msg==Cookoo }
	Z_CSP = 
		let Z(State) = [] (States,Comm) : {(com(State,c),c) | c <- Interface} @ 
				States != {} & |~| State': States @ Comm -> Z(State') 
		within  |~| iState: Init @ Z(iState) 
  within (main [|Interface|] Z_CSP)\lChannels

7. The conversion tool

Facilities

The conversion tool loads specifications from a file and splits them in two parts: CSP part and Z part. The first part is parserd by a CSP parser and the Z part is parsed by a Z one. These parsers were implemented on Laboratory of Formal Methods, using JLex and JavaCUP, scanner and parser generation tools for Java.

Limitations

Converting the CSP part to CSPM notation is a simple task, but Z structures and type definitions require a detailed study. For example

myFunction : \seq N \pfun \seq N

cannot be converted immediatelly to CSP structures and built-in types. In general, this may require many steps of data refinement to convert the Z abstract data types into the more concrete types available in CSPM. So some types and predicates will not be converted; instead, in such cases, the original specification text is reproduced into dollar signs ($). The developer has to translate these parts by hand.

8. Future versions

The tool generates automatically CSPM notation that needs little adjustments, but our efforts are focused on making the conversion process as automatic as possible. In the future versions we hope to improve in sense of provide support to splited specifications (i.e smaller specifications can be combined in a processes network). So, the specification can be checked by its smaller parts. Another improvement is turning the tool able to convert infinite processes into finite ones, without change its semantics. This technic turns several specifications able to be checked by FDR tool.

9. References

[1] Fischer C. Combining CSP and Z. Technical Report, University of Oldenburg, Germany.

[2] JLex and JavaCUP. Scanners and parsers generation tools for Java.

[3] Mota, A. & Sampaio A. Model-Checking CSP-Z: strategy, tool suport and industrial application. Science of Computer Programming, Elsevier, Netherlands. (40) 1. 2001, pp.59 - 96.

[4] Roscoe A. W.. The Theory and Practice of Concurrency. Prentice-Hall International, 1998.

[5] Scattergood B. The Semantics and Implementation of Machine-Readable CSP. PhD Thesis. University of Oxford, 1998.

[6] Martin, J.M.R. The Design and Construction of Deadlock-Free Concurrent Systems. PhD thesis. University of Buckingham, 1996.

[7] Lazic, R.A Semantic Study of Data Independence with Applications to Model-Chekcing. D. Phil. Thesis. Oxford University Computing Laboratory, 1999.

10. Download

The translator is available in two files: formw-gui.zip(with GUI) and formw-nogui.zip(command line). The GUI version needs JDK1.2.x (or later) versions. Please read the README file before use it and send us any comments about the tool. Your suggestion is very important for this software improvement. Bugs reports to Adalberto Farias, Alexandre Mota or Augusto Sampaio.