Verification of real time properties in fiacre language
type: Dataset
contact point: Organization
  fn: CCSD
keyword: pas-de-mots-cles-en-francais
keyword: observers
keyword: specification-patterns
keyword: verification
keyword: requirements
keyword: theses
keyword: infoinfo-clcomputer-science-cscomputation-and-language-cscl
keyword: model-checking
keyword: infoeu-reposemanticsdoctoralthesis
keyword: real-time-systems
landing page: https://theses.hal.science/tel-00782554
description: The formal verification of critical, reactive systems is a very complicated task, especially for non experts. In this work, we more particularly address the problem of real time systems, that is in the situation where the correctness of the system depends upon timing constraints, such as the "timeliness" of some interactions. Many solutions have been proposed to ease the specification and the verification of such systems. An interesting approach--that we follow in this thesis--is based on the definition of specification patterns, that is sets of general, reusable templates for commonly occurring classes of properties. However, patterns are rarely implemented, in the sense that the designers of specification languages rarely provide an effective verification method for checking a pattern on a system. The most common technique is to rely on a timed extension of a temporal logic to define the semantics of patterns and then to use a model-checker for this logic. However, this approach may be inadequate, in particular if patterns require the use of a logic associated to an undecidable model-checking problem or to an algorithm with a very high practical complexity. We make several contributions. We propose a complete theoretical framework to specify and check real time properties on the formal model of a system. First, our framework provides a set of real time specification patterns (that may be viewed as a timed extension of Dwyer's patterns). We provide a verification technique based on the use of observers that has been implemented in a tool for the Fiacre modelling language. Finally, we provide two methods to check the correctness of our verification approach; a "semantics"-theoretical-method as well as a "graphical"-practical- method.
issued: 2026-05-14T20:09:00.346705
language: en
modified: 2026-05-14T20:09:00.346711

test_moissonnage_selune
type: Agent

Verification of real time properties in fiacre language
type: Distribution
access URL: https://theses.hal.science/tel-00782554
format: HTML
issued: 2026-05-14T20:09:00.352776
modified: 2026-05-14T20:09:00.321431