Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application

A very simple model for train stopping is used as a vehicle for investigating how the development of a control system, initially designed in the continuous domain and subsequently discretized, can be captured within a formal development process compatible with standard model based refinement methodo...

Full description

Saved in:
Bibliographic Details
Published in:Formal aspects of computing 2014-03, Vol.26 (2), p.319-366
Main Authors: Banach, Richard, Zhu, Huibiao, Su, Wen, Huang, Runlei
Format: Article
Language:English
Subjects:
Computer Science
Control systems
Control systems design
Dealing
Discretization
Formalism
Math Applications in Computer Science
Mathematical models
Original Article
Requirements analysis
Theory of Computation
Trains
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:A very simple model for train stopping is used as a vehicle for investigating how the development of a control system, initially designed in the continuous domain and subsequently discretized, can be captured within a formal development process compatible with standard model based refinement methodologies. Starting with a formalized requirements analysis using KAOS, an abstract model of the continuous system is created in the ASM formalism. This requires extensions of the KAOS and ASM formalisms, capable of dealing with quantities evolving continuously over real time, which are developed. After considering how the continuous system, described as a continuous control system in the state space framework, can be discretized, a discrete control system is created in the state space framework. This is re-expressed in the ASM formalism. The rigorous results on the relationship between continuous and discrete control system models that are needed to establish provable properties of the discretization, then become the ingredients of a retrenchment between continuous and discrete ASM models, and are thus fully integrated into the formal development. The discrete ASM model can then be further refined towards implementation.
ISSN:0934-5043
1433-299X
DOI:10.1007/s00165-012-0263-2