uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Integrating the Z notation and behavioural formalisms
Uppsala University, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Faculty of Social Sciences, Department of Information Science.
2001 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

The last several years have witnessed an increasing interest in integrating different formalisms in the formal methods research community. Particularly a number of notations have been proposed by different authors which integrate existing state-based formalisms such as Z, VDM and B and behavioural formalisms such as CCS, CSP and Statecharts.

Those state-based formalisms are widely used both in academia and industry, but lack capabilities to capture the concurrency aspect of computer systems. On the other hand, behavioural formalisms have opposite properties, thereby it is expected that integration of both formalisms would compensate their respective shortcomings.

The integration of different formalisms was motivated by the need to integrate multiple aspects of computer systems by using corresponding formalisms. That research has raised several interesting research issues such as integration of two underlying semantics and refinement of integrated formalisms.

In this thesis, we focus on integration of the Z notation and behavioural formalisms and report two integrations, i.e., Z and first-order logics in terms of labeled transition systems, and Z and a process algebra CCS. The former integration is aimed at providing a formal language for declaring properties in Z and the latter is to give behavioural meanings to Z specifications.

Those two integrations are achieved by adopting the same semantic method in which a Z specification is embedded in a labeled transition system. Labeled transition systems are the most widely used operational (behavioural) semantic frameworks which enable us to declare constraints and properties of Z by predicate logics in terms of labeled transition systems as well as semantic integration of Z and the value-passing CCS.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis , 2001. , 30 p.
Keyword [en]
Informatics, computer and systems science, Integrated Formal Methods, CCS, Z
Keyword [sv]
Informatik, data- och systemvetenskap
National Category
Computer and Information Science
Research subject
Computer Systems
URN: urn:nbn:se:uu:diva-87ISBN: 91-506-1454-1OAI: oai:DiVA.org:uu-87DiVA: diva2:171968
Public defence
2001-02-28, Lecture hall 2, Ekonomikum, Uppsala University, Uppsala, 13:15
Available from: 2001-02-07 Created: 2001-02-07Bibliographically approved

Open Access in DiVA

No full text

By organisation
Department of Information Science
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 102 hits
ReferencesLink to record
Permanent link

Direct link