Designing a provably correct robot control system using a "lean" formal method
Date
1998
Advisors
Journal Title
Journal ISSN
ISSN
Volume Title
Publisher
Springer
Type
Book chapter
Peer reviewed
Abstract
A development method for the construction of provably correct robot control systems together with its supporting tool environment are described. The method consists of four stages: 1. specification, 2. refinement, 3. simulation and 4. code. The method is centered around the notion of wide-spectrum formalism within which an abstract Interval Temporal Logic (ITL) representation is intermixed freely with the concrete Temporal Agent Model (TAM) representation of the system under consideration. The method with its associated tool support is applied to the design of a robot control system.
Description
Keywords
EPSRC
Citation
Cau, Antonio, Czarnecki, Chrisopher Antoni and Hussein Zedan, Designing a provably correct robot control system using a "lean" formal method. In: Formal techniques in real-time and fault-tolerant systems: 5th international symposium, FTRTFT '98, Lyngby, Denmark, September 14-18, 1998: proceedings, Edited by Anders P. Ravn and Hans Rischel, Berlin: London: Springer, 1998, Lecture notes in computer science, vol.1486, pp 123-132