Rigorous code generation for distributed real-time embedded systems

• Main Author: Almohammad, Ali
• Other Authors: Kendall, David; Henderson, William
• Published: Northumbria University 2013
• Subjects: 620; G400 Computer Science
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.588280

This thesis addresses the problem of generating executable code for distributed embedded systems in which computing nodes communicate using the Controller Area Network (CAN). CAN is the dominant network in automotive and factory control systems and is becoming increasingly popular in robotic, medical and avionics applications. The requirements for functional and temporal reliability in these domains are often stringent, and testing alone may not offer the required level of con dence that systems satisfy their specications. Consequently, there has been considerable research interest in additional techniques for reasoning about the behaviour of CAN-based systems. This thesis proposes a novel approach in which system behaviour is specifed in a high-level language that is syntactically similar to Esterel but which is given a formal semantics by translation to bCANDLE, an asynchronous process calculus. The work developed here shows that bCANDLE systems can be translated automatically, via a common intermediate net representation, not only into executable C code but also into timed automaton models that can be used in the formal verification of a wide range of functional and temporal properties. A rigorous argument is presented that, for any system expressed in the high-level language, its timed automaton model is a conservative approximation of the executable C code, given certain well-defined assumptions about system components. It is shownthat an off-the-shelf model-checker (UPPAAL) can be used to verify system properties with a high-level of confidence that those properties will be exhibited by the executable code. The approach is evaluated by applying it to four representative case studies. Our results show that, for small to medium-sized systems, the generated code is sufficiently efficient for execution on typical hardware and the generated timed automaton model is sufficiently small for analysis within reasonable time and memory constraints.