Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Reports

Logical vs. Behavioural Specifications

Abstract : There are two fundamentally different approaches to specifying and verifying properties of systems. The logical approach makes use of specifications given as formulae of temporal or modal logics and relies on efficient model checking algorithms; the behavioural approach exploits various equivalence or refinement checking methods, provided the specifications are given in the same formalism as implementations. In this paper we provide translations between the logical formalism of nu-calculus and the behavioural formalism of disjunctive modal transition systems. The translations preserve structural properties of the specification and allow us to perform logical operations on the behavioural specifications as well as behavioural compositions on logical formulae. The unification of both approaches provides additional methods for component-based stepwise design.
Complete list of metadata

Cited literature [50 references]  Display  Hide  Download

https://hal.inria.fr/hal-01088150
Contributor : Uli Fahrenberg Connect in order to contact the contributor
Submitted on : Thursday, November 27, 2014 - 2:48:21 PM
Last modification on : Thursday, January 20, 2022 - 5:33:11 PM
Long-term archiving on: : Friday, April 14, 2017 - 9:53:19 PM

File

bmts.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01088150, version 1

Citation

Nikola Beneš, Uli Fahrenberg, Jan Křetínský, Axel Legay, Louis-Marie Traonouez. Logical vs. Behavioural Specifications. [Research Report] Inria Rennes. 2014. ⟨hal-01088150⟩

Share

Metrics

Record views

479

Files downloads

257