6.1.8 Model checking
The memory usage of the model checker is the current bottleneck of the system, in terms of number of tasks, processing elements and the difference between tasks best and worst case execution times. Improving the model checker in terms of less memory usage would increase the size of systems that can feasibly be verified.
A time vs. memory trade off is also interesting to investigate. A way of us-ing less memory could be to use extra space on the hard drive. This way the natural limit of 2 GB memory could be extended, on the expense of more time demanding read and write operations on the disk.
In the case where bcet=wcet, the special verifier developed by J. Illum is used.
This version does not store any visited states in order to limit the memory usage.
This however makes it impossible to calculate a schedule of the tasks, because
it is based upon the trace of states visited by the model checker, as described
in Section 3.4. A way of overcoming this problem would be to implement some
kind of print function in the UPPAAL tool. Hereby simply dump information
of visited states for each task, during verification.
Chapter 7
Conclusion
This thesis has presented a tool for formal verification of Multi-Processor Systems-on-Chip. The tool is based on a formal model using timed automata in UP-PAAL. Using model checking, properties such as schedulability, memory usage and power consumption can be verified. Using the tool, designers of embedded system are able to evaluate their design, before synthesizing in hardware. It is, in this way, possible to discover bugs earlier in the design process.
The thesis relates to the work done by A. Brekling in [4], who implemented a basic MPSoC model, capturing the concepts of dynamic scheduling and inter-processor dependencies. Our thesis has answered the objectives stated in section 1.3 and the main contributions of our work has been:
• A more realistic model for application and execution platform, by extend-ing the features which the model is able to handle with:
– Resource allocation as part of the real-time operating system.
– Non-periodic tasks (sporadic and aperiodic).
– Cost model for investigating memory usage and power consumption pr. processing elements and on the total execution platform.
– Deadline types (hard, firm, soft).
– Inter-processor communication via busses.
– Non-deterministic 1 execution times of tasks, in an interval between a best and worst case.
1
The execution times of sequential code is not in fact non-deterministic, but depends on
the input variables. However at the task level, the input variables are abstracted away and
the execution times are modelled as non-deterministic.
– Different clock frequencies on processing elements.
• Implement the timed-automata model in an efficient way, pushing the size limit of systems which can be verified. We are thus able to handle MPSoC systems of realistic sizes. It has been shown that various applications from a smart phone (114 tasks total) can be modelled and verified within 2.5 hours using a modified model checker developed by J. Illum at AAU.
• A tool, which wraps the developed timed-automata model into an easy to use program. In addition to verifying properties such as schedulability and resource usage, the tool is able to provide a schedule helping designers understanding the possible short comings of a design.
A clear division between application and execution platform has been made.
The timing properties of the application (period, deadline, offset) is defined in seconds and the execution time of the application on the execution platform is given in cycles. The period, deadline and offset is logically connected to the execution cycles through the speed of the processor.
The model has been debugged and tested using small made up cases, known examples from the literature (e.g. [20]) and a case study of the applications from a smart phone. Furthermore a size test, of systems which can be feasibly verified, is included.
The idea of using formal models for verification of MPSoCs on system-level is new. The work done in [4] showed the possibility of formal modelling and verification using timed automata. The goal of our thesis has been to develop a model which is applicable to real life problems, in terms of captured con-cepts and the size of systems. The smart phone example shows that this goal is reached. In the previous chapter, ideas of future development is presented, which will make the model even more realistic in terms of handled feature and feasible sizes of systems. Especially online task mapping is of interest as the system would be able to better adapt to unforseen events. Resources could for example be spared at times where large parts of the system is idle by grouping tasks together on fewer processing elements.
At the DATE’07 conference, we presented the work of this thesis in the
Univer-sity Booth forum. The response from fellow students and industry confirmed
our belief that, formal verification using model checking is of high interest to
companies in areas such as automotive and communications industries.
Appendix A
Terms
Task τ
Processing element pe Real-time operating system os Processor frequency f Dependency relation ≺
Application A
Execution Platform E
Set of tasks T
Set of processing elements P E
Mapping m : T → P E
Task:
Period π
Offset ω
Deadline δ
Task mapped to a pe
Best case execution time bcǫ Worst case execution time wcǫ
Period p
Offset o
Deadline d
Dynamic memory dm
Static memory sm
Power consumption pw
Appendix B
Introduction to timed automata
This appendix is written by A. Brekling and was originally included in [4], except for part 7 and 8 which have been written for the purpose of this thesis.
This introduction to timed automata is inspired by lectures and lecture notes on Process and Data Modelling by Jens Christian Godskesen, IT University of Copenhagen and on Real-Time Systems by Jesper Blak Møller, Technical University of Denmark.
In the following, it is assumed that the reader has general knowledge of finite
automata.
In document
MoVES - A tool for Modelling and Verification of Embedded Systems
(Sider 99-105)