Rigorous code generation for distributed real-time embedded systems

Almohammad, Ali (2013) Rigorous code generation for distributed real-time embedded systems. Doctoral thesis, Northumbria University.

[img]
Preview
PDF (PhD thesis)
almohammad.ali_phd.pdf - Submitted Version

Download (1MB) | Preview

Abstract

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.

Item Type: Thesis (Doctoral)
Uncontrolled Keywords: formal verification, real-time, embedded systems, controller area network, code generation
Subjects: G400 Computer Science
Department: Faculties > Engineering and Environment > Computer and Information Sciences
University Services > Graduate School > Doctor of Philosophy
Related URLs:
Depositing User: Ellen Cole
Date Deposited: 16 Dec 2013 11:49
Last Modified: 17 Dec 2023 15:22
URI: https://nrl.northumbria.ac.uk/id/eprint/14825

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year

View more statistics