A compositional analysis of broadcasting embedded systems

Brockway, Michael (2010) A compositional analysis of broadcasting embedded systems. Doctoral thesis, Northumbria University.

[img]
Preview
PDF (PhD thesis)
brockway.michael_phd.pdf - Accepted Version

Download (1MB) | Preview

Abstract

This work takes as its starting point D Kendall's CANdle/bCANdle algebraic framework for formal modelling and specification of broadcasting embedded systems based on CAN networks. Checking real-time properties of such systems is beset by problems of state-space explosion and so a scheme is given for recasting systems specified in Kendall's framework as parallel compositions of timed automata; a CAN network channel is modelled as an automaton. This recasting is shown to be bi-similar to the original bCANdle model. In the recast framework,"compositionality" theorems allow one to infer that a model of a system is simulated by some abstraction of the model, and hence that properties of the model expressible in ACTL can be inferred from analogous properties of the abstraction. These theorems are reminiscent of "assume-guarantee" reasoning allowing one to build simulations component-wise although, unfortunately, components participating in a "broadcast" are required to be abstracted "atomically". Case studies are presented to show how this can be used in practice, and how systems which take impossibly long to model-check can tackled by compositional methods. The work is of broader interest also, as the models are built as UPPAAL systems and the compositionality theorems apply to any UPPAAL system in which the components do not share local variables. The method could for instance extend to systems using some network other than CAN, provided it can be modelled by timed automata. Possibilities also exist for building it into an automated tool, complementing other methods such as counterexample- guided abstraction refinement.

Item Type: Thesis (Doctoral)
Subjects: G400 Computer Science
Department: Faculties > Engineering and Environment > Mathematics, Physics and Electrical Engineering
University Services > Graduate School > Doctor of Philosophy
Related URLs:
Depositing User: EPrint Services
Date Deposited: 16 Feb 2011 09:43
Last Modified: 24 Oct 2017 15:10
URI: http://nrl.northumbria.ac.uk/id/eprint/2967

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year

View more statistics


Policies: NRL Policies | NRL University Deposit Policy | NRL Deposit Licence