test_moissonnage_selune
type: Agent

Formal specification method for systems automation
type: Dataset
contact point: Organization
  fn: CCSD
keyword: formal-specification
keyword: requirements-analysis
keyword: automation-engineering
keyword: journal-articles
keyword: infoeu-reposemanticsarticle
keyword: formal-verification
keyword: systems-engineering
keyword: spiautoengineering-sciences-physicsautomatic
landing page: 0947-3580
description: Currently automatic control deals with the theoretical modelling techniques applied to formally define the behaviour of a control system when the system goals and the process behaviour to be controlled are well defined. Although these approaches are efficient in the design and implementation phases for controlling the dynamics of automatized systems, other tools are also required in the early stages of the process of engineering a system. This paper deals with a specification method aimed at proving that the system goals, as required by the users, are formally refined towards the real target automation system with completeness, consistency, unambiguousness and correctness guarantees. Our specification method is based on the B language to globally verify, from formal constructs, the predicate: Control Systems Requirements ⋀ Process Systems Requirements ⇒ Production System Requirements. A case study illustrates our approach and opens issues on the way to industrial practice.Currently automatic control deals with the theoretical modelling techniques applied to formally define the behaviour of a control system when the system goals and the process behaviour to be controlled are well defined. Although these approaches are efficient in the design and implementation phases for controlling the dynamics of automatized systems, other tools are also required in the early stages of the process of engineering a system. This paper deals with a specification method, based on the B language, that aims at proving that the system goals, as required by the users, are formally refined towards the real target automation system with completeness, consistency, unambiguousness and correctness guarantees. A case study illustrates our approach and opens issues on the way to industrial practice.
issued: 2026-05-07T18:30:18.743372
language: en
modified: 2026-05-07T18:30:18.743376

Formal specification method for systems automation
type: Distribution
access URL: https://hal.science/hal-00092015
format: HTML
issued: 2026-05-07T18:30:18.748362
modified: 2026-05-07T18:30:18.734499