Developing an ROV software control architecture: a formal specification approach

The software development of control architectures for Remotely Operated Vehicles (ROVs) is a complex task. The use of formal specifications for critical systems can improve both correctness and completeness of specifications and implementations. In this work, a new method for developing control architectures based on formal specifications is introduced. The chosen formal specification language is the CSP-OZ, a combination of the CSP language for behavioral model and the Object-Z language for data model. At first, the CSP parts of specifications are verified using the FDR2 model checker. Then, CSP-OZ model specifications are coded using the ADA language. More specifically, the ADA language profile Ravenscar for concurrency and the SPARK language with its annotations for data modelling are used. The SPARK annotations give support for the Object-Z specifications. Later, the SPARK examiner can be used to statically check the code against the annotations. In order to illustrate the application of the method, the development of the software control architecture of the LAURS ROV is introduced. The embedded system is based on a PCI04 Intel x86 running the real time operating system Vxworks.