Converting Ptolemy II Models to SpaceEx for Applied Verification

摘要

Developing correct models for embedded systems requires formal verification. But it increases the burden on system designers to handle the verification techniques. In this paper, we solve this problem by providing a mapping from actor models to mathematical models suitable for verification; the conversion is automatic with minimal human intervention. We have integrated a model-designing Ptolemy II tool with verification tool SpaceEx by extending syntax with hybrid aspects. The integration of both tools and enhanced expressiveness allows Ptolemy II to model hybrid systems and get them verified by SpaceEx.