Name
Abstract | ||
|---|---|---|
In this paper, we propose the use of Z as the formal notation to express Jackson System Development (JSD) specifications where JSD is to serve as the mechanism to help the analysis of problem domains. A function process in JSD specifications is manifested by an operation schema. A model process is treated as an active entity that requires an operation on its data store to add a new instance to the collection of existing instances. The model process is thus translated into a state schema, and its related operations are converted into the operation schemas with instances set that can be modified by the operations. A structure diagram is transformed into a state transition diagram and then converted into its Z specifications. Cardinality relationships between processes are translated into Z notations based upon the notion of rough merges. These are illustrated using the problem domain of Car-Rental System. |
Year | DOI | Venue |
|---|---|---|
1995 | 10.1109/CMPSAC.1995.524759 | COMPSAC |
Keywords | DocType | ISSN |
instances set,z specification,expressing jsd,related operation,model process,jsd specification,car-rental system,operation schema,jackson system development,function process,problem domain,z notation,formal specification,testing,state transition diagram,formal specifications,programming,information analysis,real time systems,kernel,software engineering,computer science | Conference | 0730-3157 |
ISBN | Citations | PageRank |
NoISBN-1 | 0 | 0.34 |
References | Authors | |
3 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| jonathan lee | 1 | 5 | 2.26 |
| wei t huang | 2 | 22 | 6.65 |
| chengkai chang | 3 | 0 | 0.34 |
| jianni pan | 4 | 107 | 4.17 |