Article View: comp.specification.z
Article #23Re: Z and concurrent systems
From: Ismar Neumann Kaufman
Date: Tue, 11 Aug 1992 22:18
Date: Tue, 11 Aug 1992 22:18
49 lines
2851 bytes
2851 bytes
In article from Aug,11, maria@dain (Maria Brielmann) writes: | I'm looking for some information about Z and specification of concurrent | systems. I heard some rumours about a special Z dialect for this task. Does | anybody of you know more details? I'm currently working on my MsC dissertation where I propose a way to join the known advantages of Z and some formal mechanism to specify concurrency. The main idea is to subvert Z semantics in order to have a structured version of modal action logic as the semantics of a Z+concurrency specification. In fact, I don't use pure Z, but the object oriented dialect MooZ, recently cited in this forum and a report of which is available via FTP. The logic is based on the work of J. Fiadeiro and T. Maibaum and includes deontic predicates for a very clean way to talk about actions occurrence. Encapsulation of data is guaranteed by a locality axiom and specifications are structured by morphisms. Objects communicate through syncronization when information may be exchanged. Fiadeiro and Maibaum have already proposed a calculus for temporal reasoning over specifications using deontic predicates. The calculus follow the structure of the specifications. Syntactically, MooZ needs very little change to incorporate modal action logic, with the addition of the two deontic predicates (for permission and obligation) and a "built-in set" called Method, which contains the names of the class methods where it occurs. In my dissertation (written in portuguese) I show how to translate MooZ specifications into modal action logic using a denotational style notation. I'm planning to have, late in September, a technical report about the language (called MaMooZ), available via ftp. Questions are welcome and if they are not of general interest, direct them to the email address below. +----------------------------------------------------------------+ | | | Ismar Neumann Kaufman Universidade Federal de Pernambuco | | ink@di.ufpe.br Departamento de Informatica | | Recife PE Brazil | | phone: +55 81 271 30 52 (lab.) | | +55 81 341 08 29 (home) | | | +----------------------------------------------------------------+
Technical Details
Message-ID:
<9208112018.AA25752@di.ufpe.br>Path:
arc1-ca.pugleaf.net!sparky!uunet!mcsun!uknet!ox-prg!inkShow Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!sparky!uunet!mcsun!uknet!ox-prg!ink From: ink@DI.UFPE.BR (Ismar Neumann Kaufman) Newsgroups: comp.specification.z Subject: Re: Z and concurrent systems Message-ID: <9208112018.AA25752@di.ufpe.br> Date: 11 Aug 92 22:18:54 GMT Sender: daemon@comlab.ox.ac.uk Lines: 49 X-Envelope-To: zforum@prg.oxford.ac.uk X-Mailer: mail-news 2.0.3