Top

Published in:

2020 | OriginalPaper | Chapter

Refinement and Verification of Responsive Control Systems

Authors : Karla Morris, Colin Snook, Thai Son Hoang, Geoffrey Hulette, Robert Armstrong, Michael Butler

Published in: Rigorous State-Based Methods

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Statechart notations with ‘run to completion’ semantics, are popular with engineers for designing controllers that respond to events in the environment with a sequence of state transitions. However, they lack formal refinement and rigorous verification methods.

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-48077-6_23/MediaObjects/489038_1_En_23_Figa_HTML.gif

, on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible. We introduce a notion of refinement into a ‘run to completion’ statechart modelling notation, and leverage

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-48077-6_23/MediaObjects/489038_1_En_23_Figb_HTML.gif

tool support for theorem proving. We describe the difficulties in translating ‘run to completion’ semantics into

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-48077-6_23/MediaObjects/489038_1_En_23_Figc_HTML.gif

refinements and suggest a solution. We outline how safety and liveness properties could be verified.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Towards a Shared Specification Repository

next chapter Adaptive Exterior Light and Speed Control System

ProB is an animator, constraint solver and model checker for the B-Method. https://www3.hhu.de/stups/prob.

Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRef

Syriani, L.L.E., Sousa, V.: Structure and behavior preserving statecharts refinements. Sci. Comput. Program. 170(15), 45–79 (2019)CrossRef

Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987)MathSciNetCrossRef

Hoang, T.S.: An introduction to the Event-B modelling method. In: Romanovsky, A., Thomas, M. (eds.) Industrial Deployment of System Engineering Methods, pp. 211–236. Springer, Heidelberg (2013)

Maraninchi, F.: The Argos language: graphical representation of automata and description of reactive systems. In: IEEE Workshop on Visual Languages (1991)

MATLAB. 9.7.0.1190202 (R2019b). The MathWorks Inc., Natick, Massachusetts (2019)

Morris, K., Snook, C.: Reconciling SCXML statechart representations and Event-B lower level semantics. In: HCCV - Workshop on High-Consequence Control Verification (2016)

Morris, K., Snook, C., Hoang, T.S., Armstrong, R., Butler, M.: Refinement of statecharts with run-to-completion semantics. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2018. CCIS, vol. 1008, pp. 121–138. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-12988-0_8CrossRef

Said, M.Y., Butler, M., Snook, C.: A method of refinement in UML-B. Softw. Syst. Model. 14(4), 1557–1580 (2015)CrossRef

10.

Snook, C.: iUML-B statemachines. In: Proceedings of the Rodin Workshop 2014, Toulouse, France, pp. 29–30 (2014). http://eprints.soton.ac.uk/365301/

11.

Snook, C., Butler, M.: UML-B: formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006)CrossRef

12.

W3C. State chart XML SCXML: State machine notation for control abstraction, September 2015. http://www.w3.org/TR/scxml/

Title: Refinement and Verification of Responsive Control Systems
Authors: Karla Morris
Colin Snook
Thai Son Hoang
Geoffrey Hulette
Robert Armstrong
Michael Butler
Publisher: Springer International Publishing
Book: Rigorous State-Based Methods
Print ISBN: 978-3-030-48076-9

Electronic ISBN: 978-3-030-48077-6

Copyright Year: 2020
DOI: https://doi.org/10.1007/978-3-030-48077-6_23

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner