Bibliography

[GHK+04] Heterogeneous formal specification based on Object-Z and statecharts: semantics and verification

Gruer.jss04 (Article)
Author(s)	Gruer, Pablo and Hilaire, Vincent and Koukam, Abder and Rovarini, P.
Title	« Heterogeneous formal specification based on Object-Z and statecharts: semantics and verification »
Journal	Journal of Systems and Software
Volume	70
Number	1-2
Page(s)	95--105
Year	2004

Gruer.jss04 (Article)

Author(s)

Gruer, Pablo and Hilaire, Vincent and Koukam, Abder and Rovarini, P.

Title

« Heterogeneous formal specification based on Object-Z and statecharts: semantics and verification »

Journal

Journal of Systems and Software

Volume

Number

1-2

Page(s)

95--105

Year

2004

Abstract & Keywords
This work presents a specification language, called OZS, based on two formalisms: Object-Z and the statecharts. Such a specification style facilitates the modeling of systems with both reactive and functional aspects. The accent is placed on OZS semantics so as to give formal foundations to verification and simulation of OZS models. Every OZS model has a transition system as its semantic interpretation. Untimed and timed versions of the OZS semantics are presented. Both transition system models of an OZS class can be used for verification purposes by model checking. In this work, a real-word example is treated and the resulting specification is model-checked by using the Stanford Temporal Prover environment from Stanford. Keywords: Object-Z, statecharts, transition systems, model-checking

Abstract & Keywords

This work presents a specification language, called OZS, based on two formalisms: Object-Z and the statecharts. Such a specification style facilitates the modeling of systems with both reactive and functional aspects. The accent is placed on OZS semantics so as to give formal foundations to verification and simulation of OZS models. Every OZS model has a transition system as its semantic interpretation. Untimed and timed versions of the OZS semantics are presented. Both transition system models of an OZS class can be used for verification purposes by model checking. In this work, a real-word example is treated and the resulting specification is model-checked by using the Stanford Temporal Prover environment from Stanford.

Keywords: Object-Z, statecharts, transition systems, model-checking

BibTeX code

@article{Gruer.jss04,
  number = {1-2},
  volume = {70},
  author = {Gruer, Pablo and Hilaire, Vincent and Koukam, Abder and Rovarini,
            P.},
  domains = {Multi-Agent Systems:Formal Specification/OZS:},
  title = {Heterogeneous formal specification based on Object-Z and statecharts:
           semantics and verification},
  year = 2004,
  pages = {95--105},
  journal = {Journal of Systems and Software},
}

Documents in the same domains

Root

Formal Specification/OZS

		[GHK+00] Gruer P. et al., "Verification of Object-Z Specifications..." (2000)
		[GHK+02] Gruer P. et al., "A formal framework for multi-agent..." (2002)
		[GHK+04] Gruer P. et al., "Heterogeneous formal specification based..." (2004)
		[HKG+01] Hilaire V. et al., "Formal Specification and Prototyping of..." (2001)
		[HKG+01b] Hilaire V. et al., "Vers une méthodologie formelle de..." (2001)

Multi-Agent Systems

		[DC+95] Donikian S. et al., "General Animation and Simulation Platform" (1995)
		[DOO+99] Duffy B.R. et al., "Reality and virtual reality in mobile..." (1999)
		[DVM+02] Drogoul A. et al., "Multi-Agent Based Simulation: Where are..." (2002)
		[ELW+03] Erol K. et al., "Application of Agent Technology to..." (2003)
		[GBR+95] Granieri J.P. et al., "Behavioral Control for Real-Time..." (1995)
		[GGB+03] Galland S. et al., "MaMA-s: An introduction to a..." (2003)
		[GHK+00] Gruer P. et al., "Verification of Object-Z Specifications..." (2000)
		[GHK+02] Gruer P. et al., "A formal framework for multi-agent..." (2002)
		[GHK+04] Gruer P. et al., "Heterogeneous formal specification based..." (2004)
		[HKG+01] Hilaire V. et al., "Formal Specification and Prototyping of..." (2001)
		[HKG+01b] Hilaire V. et al., "Vers une méthodologie formelle de..." (2001)
		[HU+01] Henoch J. et al., "Agent-based Simulation Platform for..." (2001)
		[IB+02] Isla D. et al., "New challenges for character-based ai..." (2002)
		[PB+99] Phillips C.T. et al., "A Cooperative Human-Adaptive Traffic..." (1999)
		[PBS+05] Parunak H.V.D. et al., "Global Convergence of Local Agent..." (2005)
		[VD+02] Vanbergue D. et al., "Approche multi-agent pour la simulation..." (2002)