DocumentCode :
3863076
Title :
Hierarchical multi-formalism proofs of cyber-physical systems
Author :
Michael W. Whalen;Sanjai Rayadurgam;Elaheh Ghassabani;Anitha Murugesan;Oleg Sokolsky;Mats P.E. Heimdahl;Insup Lee
Author_Institution :
Department of Computer Science and Engineering, University of Minnesota
fYear :
2015
Firstpage :
90
Lastpage :
95
Abstract :
To manage design complexity and provide verification tractability, models of complex cyber-physical systems are typically hierarchically organized into multiple abstraction layers. High-level analysis explores interactions of the system with its physical environment, while embedded software is developed separately based on derived requirements. This separation of low-level and high-level analysis also gives hope to scalability, because we are able to use tools that are appropriate for each level. When attempting to perform compositional reasoning in such an environment, care must be taken to ensure that results from one tool can be used in another to avoid errors due to “mismatches” in the semantics of the underlying formalisms. This paper proposes a formal approach for linking high-level continuous time models and lower-level discrete time models.
Keywords :
"Automata","Contracts","Semantics","Clocks","Cost accounting","Synchronization","Cognition"
Publisher :
ieee
Conference_Titel :
Formal Methods and Models for Codesign (MEMOCODE), 2015 ACM/IEEE International Conference on
Type :
conf
DOI :
10.1109/MEMCOD.2015.7340474
Filename :
7340474
Link To Document :
بازگشت