Using sharing trees in the automated analysis of real-time systems with data

Kendall, David, Henderson, William and Robson, Adrian (1999) Using sharing trees in the automated analysis of real-time systems with data. IEE Colloquium (Digest) (6). pp. 21-24. ISSN 0963-3308

Full text not available from this repository. (Request a copy)

Abstract

Reachability analysis and model checking of timed automata are now well-established techniques in the analysis of real-time control systems. The major limiting factor in their use, from a technical point of view, remains the state explosion problem. Symbolic representation of the state space often allows for the analysis of much larger systems than the point-wise representation which is common in enumerative analysis. In particular, the use of rooted, ordered binary decision diagrams (ROBDDs) has been successful, mainly in the analysis of hardware systems where the need for a compact representation of boolean functions is prevalent. However in software systems, it is often desirable to represent data types which are more complicated than booleans. The use of sharing trees [16], which eliminates the requirement to find a boolean encoding of all data types, may offer a more attractive alternative to ROBDDs in these circumstances. This paper considers the use of sharing trees in the context of automata derived from a timed algebra of asynchronous broadcasting systems. It suggests that an encoding of timing constraints may be more easily incorporated into a sharing tree representation of the state space than into one based on ROBDDs.

Item Type:	Article
Additional Information:	IEE Colloquium on Applicable Modelling, Verification and Analysis Techniques for Real-Time Systems (Ref. No. 1999/006)held on 11 January 1999 in London
Subjects:	H600 Electronic and Electrical Engineering
Department:	Faculties > Engineering and Environment > Mathematics, Physics and Electrical Engineering
Depositing User:	Becky Skoyles
Date Deposited:	26 Jan 2015 10:59
Last Modified:	12 Oct 2019 19:05
URI:	http://nrl.northumbria.ac.uk/id/eprint/20414

Downloads