Designing a provably correct robot control system using a "lean" formal method
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.
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
ISBN : 3540650032
Research Group : Software Technology Research Laboratory (STRL)