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. |
Year | DOI | Venue |
---|---|---|
2015 | 10.1109/MEMCOD.2015.7340474 | MEMOCODE |
Keywords | Field | DocType |
hierarchical multiformalism proofs,design complexity,verification tractability,complex cyber-physical systems,abstraction layers,physical environment,embedded software,low-level analysis,high-level analysis,compositional reasoning,high-level continuous time models,lower-level discrete time models | Embedded software,Computer science,Automaton,Real-time computing,Theoretical computer science,Cyber-physical system,Mathematical proof,Discrete time and continuous time,Rotation formalisms in three dimensions,Semantics,Scalability | Conference |
Citations | PageRank | References |
0 | 0.34 | 21 |
Authors | ||
7 |
Name | Order | Citations | PageRank |
---|---|---|---|
Michael W. Whalen | 1 | 1096 | 70.54 |
Sanjai Rayadurgam | 2 | 284 | 29.86 |
Elaheh Ghassabani | 3 | 18 | 2.72 |
Anitha Murugesan | 4 | 44 | 5.21 |
oleg sokolsky | 5 | 7 | 1.99 |
Mats Per Erik Heimdahl | 6 | 538 | 66.59 |
Insup Lee | 7 | 4996 | 413.64 |