MoVES — A framework for modelling and verifying embedded systems

The MoVES framework is being developed to assist in the early phases of embedded systems design. A system is modelled as an application running on an execution platform. The application is modelled through the individual tasks, and the execution platform is modelled through the processing elements, including the operating systems, and their interconnections. The tasks and processing elements are characterized by their real-time properties. The framework can be used to conduct schedulability analysis and has the potential to reason about different types of resource usage such as memory usage and power consumption. A simple specification language for embedded systems and a verification backend are presented. The framework has a modular, parameterized structure supporting easy extension and adaptation of the specification language as well as of the verification backend. We show, using a number of small examples, how MoVES can be used to model and analyze embedded systems.