Jan Broenink: Embedded Control Software Design with Formal Methods and Engineering Models
Joint seminar BCS-FACS with FME, September 13th 2010
The speaker presented ongoing work in the model driven design of embedded control software, entailing both dependability and safety. Such systems contain both continuous time (CT) and discrete event (DE) elements. During the seminar a test case, a production cell demonstrator, was also described for which two types of control computer had been tried and compared: a central processing unit (CPU) and a programmable integrated circuit (a Field Programmable Gate Array or FPGA).
Both CT and DE related formal methods had been utilised in the design of software for the demonstrator, including respectively bond graphs and CSP. Bond graphs are labelled and directional graphs based on energy exchange and are capable of generating equations (both ordinary differential and algebraic) and block diagrams. CSP and its graphical tool gCSP was used to model DE elements, together with the refinement checker FDR2. The CT and DE models were then integrated and realised to form ECS software, the two types of model being combined in co-simulation.
The case study (a Stork plastic moulding machine) was presented together with the problems encountered. The production process comprised moulding, extraction, transportation, storage where synchronisation was required of neighbouring processes and deadlock was possible for several blocks. The conclusions of the study were that there was a trade-off between the two types of computer: for the CPU, the design times were shorter but the real time behaviour was critical, while for the FPGA the design time was higher and black box debugging more difficult. However use of the FPGA resulted in more accurate timing. Overall however, valuable information for improvement of design methods and for tooling was gathered by the study- it was noted that gCSP version 2 was being developed.
REPORT: Dr Margaret West (BCS-FACS), University of Huddersfield