Safety-critical design of the Generic Driving Actuator : a hybrid approach
Leon Merkx, Hans-Martin Duringhof, Pjl Pieter Cuijpers · TU/e Research Portal · 2007
The software of the GDA needs to be correct under all circumstances to guarantee its safety. Therefore the software is designed and verified using formal methods. First the requirements of the software are specified. Based on these requirements a software model is built in the proces-algebraic language μCRL. The requirements are then converted to modal logic, which can be verified against the software model.