Modern real-time languages such as Ada [139], Chill [18], Occam [76] and Conic [65,79] typically have delay and timeout features for implementing timing constraints. In addition, these languages incorporate features such as task decomposition, abstraction (information hiding), communication and concurrency mechanisms that simplify the description of complex controller software.
For example, in Ada, a module can be decomposed into several tasks. A task can be further divided into two parts: the task specification and the body of the task. During initial program development, only the specification part of the tasks needs to be defined. The specification parts can be compiled to check for overall controller consistency. Later, the task bodies can be specified in more detail. The specification part is done by senior designers, because the specification represents the interface between software components. An error in such code may therefore have more serious ramifications than an error within a task body. A task can then be given to a junior programmer for coding.
Conic implements several useful reconfiguration primitives. The primitives allow for dynamic insertion or deletion of tasks or modules, while the rest of the system continues to run. Thus maintenance to controller software can be implemented without shutting down the plant. Occam has been used as a target language for process algebras (see Section 5.2).
The advantage of these languages is that at the end of the design process, the controller is available in directly executable code. However, most real-time programming languages lack an underlying abstract mathematical model. As a result the precise semantics is unspecified or even uncertain, and there is a proliferation of irrelevant detail not needed at the level of abstract specification. Usually the code must be converted into a formal notation (e.g. Petri Nets) before the code can be verified. If these languages alone are used, then the plant is not usually represented, although pseudo plant processes can be coded. Thus there is no method to formally verify whether the controller satisfies the requirements specification S.