Show all publications

Heterogeneous Formal Specification Based on Object-Z and State Charts: Semantics and Verification

Download Bibliography in Open DocumentDownload Bibliography in HTMLDownload BibTeXDownload RISDownload Bibliographical Ontology (RDF)
In Journal of Systems and Software, vol. 70(1-2), pp. 95-105, Elsevier, 2004.
This work presents a specification language, called OZS, based on two formalisms: Object-Z and the statecharts. Such a spec- ification 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.
Object-Z; Statecharts; Transition systems; Model-checking
Publication Category:
International journal with reading committee
Copyright 2010-2019 © Laboratoire Connaissance et Intelligence Artificielle Distribu√©es - Université Bourgogne Franche-Comté - Privacy policy