From POOSL to UPPAAL : transformation and quantitative analysis
| Autor: | Xing, Jiansheng, Theelen, B.D., Langerak, Rom, van de Pol, Jaco, Tretmans, Jan, Voeten, J.P.M., Gomes, L., Khomenko, V., Fernandes, J.M. |
|---|---|
| Přispěvatelé: | Electronic Systems |
| Jazyk: | angličtina |
| Rok vydání: | 2010 |
| Předmět: |
Model checking
Modeling language Design space exploration Computer science Performance Real-time computing 02 engineering and technology Transformation EC Grant Agreement nr.: FP7/214755 CR-B.2.2 0202 electrical engineering electronic engineering information engineering POOSL Quantitative analysis FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS RapidIO Network packet Verification 020207 software engineering Specification language Motion control Automaton UPPAAL Computer engineering CR-B.8 020201 artificial intelligence & image processing EC Grant Agreement nr.: FP7-ICT-2007-1 |
| Zdroj: | STARTPAGE=47;ENDPAGE=56;TITLE=10 International Conference on Application of Concurrency to System Design ACSD Proceedings of the 10th International Conference on Application of Concurrency to System Design (ACSD 2010), 21-25 June 2010, Braga, Portugal, 47-56 STARTPAGE=47;ENDPAGE=56;TITLE=Proceedings of the 10th International Conference on Application of Concurrency to System Design (ACSD 2010), 21-25 June 2010, Braga, Portugal |
| Popis: | POOSL (Parallel Object-Oriented Specification Language) is a powerful general purpose system-level modeling language. In research on design space exploration of motion control systems, POOSL has been used to construct models for performance analysis. The considered motion control algorithms are characterized by periodic execution. They are executed by multiple processors, which are interconnected by Rapid Input/Output (RapidIO) packet switches. Packet latencies as worst-case latencies and average-case latencies are essential performance criteria for motion control systems. However, POOSL analysis merely allows for estimation results for these latency metrics since it is primarily based on simulation. Because motion control systems are time-critical and safety-critical, worst-case latencies of packets are strict timing constraints. Therefore exact worst-case latencies are to be determined. Motivated by this requirement we propose to use model checking techniques. In this paper we illustrate how a POOSL model of a (simplified) motion control system can be transformed into an UPPAAL model and we verify its functional behavior and worst-case latencies. Moreover, we show that analysis of average-case latencies can also be accomplished with assistance of the model checking tool UPPAAL. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|