Verification of Distrubuted Systems
Problem statement
Figure 8-15 illustrates mayor topic of verification of distributed systems . Figure shows a control system consisting of n independent processors and communication bus with general communication protocol. Let us consider the parallel machines running applications in the real-time operating system (RTOS) environment and further let us consider the communication protocol behaving in Real-time manner. The crucial problem is whether the general real-time control system (RTCS) [Buttazzo97] behaves in this manner too.
For simplicity we suppose that each processor is running only one task so there is no problem with scheduling. And further let us suppose the communication protocol to be deterministic (CAN, Token ring etc.).
To resolve the above mentioned problem we use a mathematics formalisms based on Petri Nets and communicating automata theory. Especially we use the tools that have been already used to solve similar problems (PEP tool, UPAAL etc.). The tools are able to model concurrent systems and mainly verify it. To reach the mentioned goal we need to create model of RTCS. The work includes the model of the communication protocol, the model of RTOS and the model of the application. After that we create model of RTCS. Finally we need correctly define dangerous system properties that can assign the system to undesirable states (Deadlock, missing deadline etc.).
Such model plus properties to be verified will be passed to the verification tools, exactly verified with included methods (SPIN algorithm, temporal logic, etc.). Due to the model checking we can say that the system can avoid the states.
Modelling of communication protocol
We are modelling and verifying a communicating system we have to understand the idea of communication protocol design [Holzmann91]. At the start of the design we must answer the next five questions:
What service should be provided by the protocol?
What assumptions are about the environment in which the protocol is executed?
What vocabulary of messages should be used to implement the protocol?
What encoding (format) of each message in the vocabulary should be used?
What procedure rules are guarding the consistency of message exchanges?
If we satisfactorily answer the questions we can suggest concrete structure of communication protocol. During solving of the question problem we have to ask for kind of properties of the protocol. For example type of transmission of bits over a physical circuit, error-control problem, flow-control problem and so on. It is evident that the most complicated design problem the most difficult his resolving. Partitioning the problem to small subproblems is reason that tell us common sense. The subproblems can be either easy to solve or they have been solved before. One of them can be ISO/OSI model of protocol layers, encoding of messages (e.i. CRC) or access control at physical media (i.e. MAC).
In OCERA project we are interested in CAN bus communication protocol due to its real-time properties (see "Survey on RTOS"). The protocol will be modelled and it will be included to RTCS as communication part.
Model of RTOS
The term real-time is frequently used in many application fields. The definitions [Buttazzo97] adopted by us is that the main difference between a real-time and non-real-time task is that the real-time is characterised by a deadline, which is the maximum time within which it must complete its execution. In critical applications, a result produced after the deadline is not late but wrong! RTOS is operating system in manner of the definition.
We need RTOS model in this point of view. The model connects application part and communication part of RTCS verified by verification tools.
Tools
To modelling and verifying the models above we use a tools that are allowed do that with sophisticated mathematical formalisms. This tools are based on Petri Net or communicating automata and they proved their qualities in research community. Our intention is to use them in applications based on RTOS and fieldbus systems.
PEP tool
PEP tool (Programming Environment based on Petri nets) [Best98] [PEP] is able to model concurrent systems and to verify them by partial model checking based on a compositional denotation Petri nets semantics. The language supported by the tools covers block structuring, parallel and sequential composition, synchronous and asynchronous communications and so on.
Modelling allows to create either graphical version of Petri net model or structured program code of the model in B(PN)2 (Basic Petri Net Programming Notation) [Best83] or SDL (Specification and Description Language) [PEP].
PEP contains those verification components:
FC2Tools (verification based on networks automata)
SMV (CTL model checking)
SPIN (linear temporal logic with optional partial order reduction)Deadlock free checker
UPPAAL
UPPAAL [UPPAAL]allows modelling, simulation and verification of real-time systems. It is appropriate for systems that can be modelled as collection of non-deterministic processes with finite control structure and real-valued clocks, communicating through channels or shared variables.
Typical application areas of the tool include real-time controllers and communication protocols in particular, those where timing aspects are critical.
Remarks
The goal of our work is to use the proved tools to create some models of OCERA software components. A future application developer will need to create only a model of his application tasks and to define the model properties to be verified.
The essential part of the work will be an example of the RT application, its model and properties verification.
Bibliography
[[Holzmann91]] Gerard J. Holzmann, 1991, Prentice Hall, Design and validation of computer protocols.
[[Buttazzo97]] Giorgios C. Buttazzo, 1997, Kluwer Academic Publisher, Hard Real-time computing systems: Predictable Scheduling Algorithms and Applications.