Statecharts for Reconfigurable Modular Control of Complex Reactive Systems: need for formal verification and associated problems

Several formal tools for specifying the control of complex reactive systems have been proposed. Modelling languages, like UML describe high-level structure and behaviour, rather than implementation of solutions. Simulators can help to validate systems, i.e., discover design flaws, if they occur in a...

Full description

Saved in:
Bibliographic Details
Main Author: Devapriya Dewasurendra, S.
Format: Conference Proceeding
Language:English
Subjects:
Automatic control
Communication system control
Computational modeling
Computer errors
Computer science
Control systems
Control theory
Formal verification
Testing
Unified modeling language
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Several formal tools for specifying the control of complex reactive systems have been proposed. Modelling languages, like UML describe high-level structure and behaviour, rather than implementation of solutions. Simulators can help to validate systems, i.e., discover design flaws, if they occur in a simulation session. Similar to testing, simulators cannot show the absence of errors. In contrast, formal verification establishes correctness by mathematical proof. The field of discrete event dynamic systems has emerged at the confluence of systems and control theory and formal computer science as the application of systems and control theory to discrete state, event-driven systems. Many aspects of this model have been studied. The base model is always the finite state machine in its different forms or equivalently, language models. This body of research represents the most comprehensive set of formal verification and validation tools in controller design for asynchronous event-driven systems up to now. The statechart model extends state machines along three orthogonal dimensions - hierarchy, concurrency and communication - resulting in a compact visual notation that allows engineers to structure and modularise system descriptions. The resulting complex semantics make automated verification of statechart models a difficult and hence, largely an unresolved problem. The current communication presents the need for modular specification and verification methodologies applicable to statechart based controllers for reconfigurable reactive systems and the problems characterising them. This research points to new strategies capable of addressing the identified problems
ISSN:2164-7011
2690-3423
DOI:10.1109/ICIIS.2006.365735