Subscribe

Issue No.06 - November/December (2011 vol.37)

pp: 826-844

Laura Carnevali , Università di Firenze, Firenze

Lorenzo Ridi , Università di Firenze, Firenze

Enrico Vicario , Università di Firenze, Firenze

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2011.4

ABSTRACT

Preemptive Time Petri Nets (pTPNs) support modeling and analysis of concurrent timed SW components running under fixed priority preemptive scheduling. The model is supported by a well-established theory based on symbolic state space analysis through Difference Bounds Matrix (DBM) zones, with specific contributions on compositional modularization, trace analysis, and efficient overapproximation and cleanup in the management of suspension deriving from preemptive behavior. In this paper, we devise and implement a framework that brings the theory to application. To this end, we cast the theory into an organic tailoring of design, coding, and testing activities within a V-Model SW life cycle in respect of the principles of regulatory standards applied to the construction of safety-critical SW components. To implement the toolchain subtended by the overall approach into a Model Driven Development (MDD) framework, we complement the theory of state space analysis with methods and techniques supporting semiformal specification and automated compilation into pTPN models and real-time code, measurement-based Execution Time estimation, test case selection and execution, coverage evaluation.

INDEX TERMS

Real-time systems, safety-critical SW components, SW life cycle, V-Model, preemptive Time Petri Nets, symbolic state space analysis, model driven development, automated model transformation, automated code generation, Execution Time estimation, real-time testing, test case selection and execution, coverage analysis.

CITATION

Laura Carnevali, Lorenzo Ridi, Enrico Vicario, "Putting Preemptive Time Petri Nets to Work in a V-Model SW Life Cycle",

*IEEE Transactions on Software Engineering*, vol.37, no. 6, pp. 826-844, November/December 2011, doi:10.1109/TSE.2011.4REFERENCES

- [1] A. Bertolino and M. Marré, "Automatic Generation of Path Covers Based on the Control Flow Analysis of Computer Programs,"
IEEE Trans. Software Eng., vol. 20, no. 12, pp. 885-899, Dec. 1994.- [2] A. Burns, B. Dobbing, and T. Vardanega, "Guide on the Use of the ADA Ravenscar Profile in High Integrity Systems,"
ADA Letters, vol. 24, no. 2, pp. 1-74, 2004.- [3] A. Colin and I. Puaut, "A Modular and Retargetable Framework for Tree-Based WCET Analysis,"
Proc. 13th Euromicro Conf. Real-Time Systems, pp. 37-44, June 2001.- [4] A. Hessel, K. Larsen, B. Nielsen, P. Pettersson, and A. Skou, "Time-Optimal Realtime Test Case Generation Using UPPAAL,"
Proc. Int'l Workshop Formal Approaches to Testing of Software, 2003.- [5] AbsIntAngewandte Informatik GmbH,
aiT Worst-Case Execution Time Analyzers, www.absint.comait, 2011.- [6] R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine, "The Algorithmic Analysis of Hybrid Systems,"
Theoretical Computer Science, vol. 138, pp. 3-34, 1995.- [7] R. Alur, I. Lee, and O. Sokolsky, "Compositional Refinement for Hierarchical Hybrid Systems,"
Proc. Int'l Workshop Hybrid Systems: Computation and Control, pp. 33-48, 2001.- [8] A. Hessel and P. Pettersson, "A Global Algorithm for Model-Based Test Suite Generation,"
Electronic Notes in Theoretical Computer Science, vol. 190, no. 2, pp. 47-59, 2007.- [9] B. Berthomieu, D. Lime, O.H. Roux, and F. Vernadat, "Reachability Problems and Abstract State Spaces for Time Petri Nets with Stopwatches," LAAS Report 04483, 2004.
- [10] B. Berthomieu and M. Diaz, "Modeling and Verification of Time Dependent Systems Using Time Petri Nets,"
IEEE Trans. Software Eng., vol. 17, no. 3, pp. 259-273, Mar. 1991.- [11] B. Berthomieu and M. Menasche, "An Enumerative Approach for Analyzing Time Petri Nets,"
Information Processing: Proc. IFIP Congress 1983, R.E.A. Mason, ed., vol. 9, pp. 41-46, 1983.- [12] BWB- Fed. Office for Military Technology and Procurement of Germany, "V-Model 97, Lifecycle Process Model-Developing Standard for IT Systems of the Fed. Republic of Germany,"
General Directive No. 250, June 1997.- [13] CENELEC,
EN 50128—Railway Applications: SW for Railway Control and Protection Systems, 1997.- [14] K. Czarnecki and S. Helsen, "Feature-Based Survey of Model Transformation Approaches,"
IBM Systems J., vol. 45, pp. 621-645, July 2006.- [15] Dept. of Aerospace Eng.—Polytechnic of Milan,
RTAI: Real Time Application Interface for Linux, https:/www.rtai.org, 2011.- [16] D.C. Schmidt, "Model-Driven Engineering,"
Computer, vol. 39, no. 2 pp. 25-31, Feb. 2006.- [17] E. Fersman, P. Pettersson, and W. Yi, "Timed Automata with Asynchronous Processes: Schedulability and Decidability,"
Proc. Eighth Int'l Conf. Tools and Algorithms for Construction and Analysis of Systems, 2002.- [18] E. Vicario, "Static Analysis and Dynamic Steering of Time Dependent Systems Using Time Petri Nets,"
IEEE Trans. Software Eng., vol. 27, no. 1, pp. 728-748, Aug. 2001.- [19] F. Cassez, A. David, E. Fleury, K.G. Larsen, and D. Lime, "Efficient On-the-Fly Algorithms for the Analysis of Timed Games,"
Proc. Int'l Conf. Concurrency Theory, pp. 66-80, 2005.- [20] F. Cassez and K.G. Larsen, "The Impressive Power of Stopwatches,"
Proc. Int'l Conf. Concurrency Theory, Aug. 2000.- [21] F.M. Proctor and W.P. Shackleford, "Real-Time Operating System Timing Jitter and Its Impact on Motor Control,"
Proc. SPIE Sensors and Controls for Intelligent Manufacturing II, vol. 4563, pp. 10-16, Dec. 2001.- [22] E. Fersman, P. Krcal, P. Pettersson, and W. Yi, "Task Automata: Schedulability, Decidability and Undecidability,"
Information and Computation, vol. 205, no. 8, pp. 1149-1172, 2007.- [23] G. Behrmann, A. David, and K.G. Larsen, "A Tutorial on Uppaal,"
Proc. Fourth Int'l School on Formal Methods for the Design of Computer, Comm., and Software Systems, pp. 200-236, Sept. 2004.- [24] G. Bernat, R.I. Davis, N. Merriam, J. Tuffen, A. Gardner, M. Bennett, and D. Armstrong, "Identifying Opportunities for Worst-Case Execution Time Reduction in an Avionics System,"
Ada User J., vol. 28, no. 3, pp. 189-194, Sept. 2007.- [25] G. Bucci, A. Fedeli, L. Sassoli, and E. Vicario, "Modeling Flexible Real Time Systems with Preemptive Time Petri Nets,"
Proc. 15th Euromicro Conf. Real-Time Systems, July 2003.- [26] G. Bucci, A. Fedeli, L. Sassoli, and E. Vicario, "Timed State Space Analysis of Real Time Preemptive Systems,"
IEEE Trans. Software Eng., vol. 30, no. 2, pp. 97-111, Feb. 2004.- [27] G. Bucci, L. Carnevali, L. Ridi, and E. Vicario, "Oris: A Tool for Modeling, Verification and Evaluation of Real-Time Systems,"
Int'l J. Software Tools for Technology Transfer, vol. 12, no. 5, pp. 391-403, 2010.- [28] G. Buttazzo,
Hard Real-Time Computing Systems. Springer, 2005.- [29] G. Karsai, J. Sztipanovits, A. Ledeczi, and T. Bapty, "Model-Integrated Development of Embedded Software,"
Proc. IEEE, vol. 91, no. 1, pp. 145-164, Jan. 2003.- [30] H. Muccini, A. Bertolino, and P. Inverardi, "Using Software Architecture for Code Testing,"
IEEE Trans. Software Eng., vol. 30, no. 3, pp. 160-171, Mar. 2004.- [31] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi, "HyTech: A Model Checker for Hybrid Systems,"
Software Tools for Technology Transfer, vol. 1, pp. 460-463, 1997.- [32] T.A. Henzinger, C.M. Kirsch, M.A.A. Sanvido, and W. Pree, "From Control Models to Real-Time Code Using Giotto,"
IEEE Control Systems, vol. 23, no. 1, pp. 50-64, Feb. 2003.- [33] I. Stuermer, M. Conrad, H. Doerr, and P. Pepper, "Systematic Testing of Model-Based Code Generators,"
IEEE Trans. Software Eng., vol. 33, no. 9, pp. 622-634, Sept. 2007.- [34] I. Wenzel, R. Kirner, B. Rieder, and P. Puschner, "Measurement-Based Timing Analysis,"
Proc. Int'l Symp. Leveraging Applications of Formal Methods, Verification and Validation, Oct. 2008.- [35] Int'l Software Testing Qualifications Board,
Standard Glossary of Terms Used in Software Testing—v2.0, 2007.- [36] J.A. Stankovic, M. Spuri, K. Ramamritham, and G.C. Buttazzo,
Deadline Scheduling for Real-Time Systems: EDF and Related Algorithms. Kluwer Academic Publishers, 1998.- [37] J.J. Chilenski and S.P. Miller, "Applicability of Modified Condition/Decision Coverage to Software Testing,"
Software Eng. J., vol. 29, no. 5, pp. 193-200, 1994.- [38] J. McManis and P. Varaiya, "Suspension Automata: A Decidable Class of Hybrid Automata,"
Proc. Sixth Int'l Conf. Computer Aided Verification, June 1994.- [39] J. Staschulat, R. Ernst, A. Schulze, and F. Wolf, "Context Sensitive Performance Analysis of Automotive Applications,"
Proc. Conf. Design, Automation and Test in Europe, Mar. 2005.- [40] J. Tretmans, "Test Generation with Inputs, Outputs, and Quiescence,"
Proc. Int'l Workshop Tools and Algorithms for the Construction and Analysis of Systems, pp. 127-146, 1996.- [41] K. Altisen, G. Goessler, and J. Sifakis, "Scheduler Modeling Based on the Controller Synthesis Paradigm,"
Real-Time Systems, vol. 23, pp. 55-84, 2002.- [42] K. Larsen, M. Mikucionis, and B. Nielsen, "Online Testing of Real-Time Systems Using Uppaal: Status and Future Work,"
Proc. Perspectives of Model-Based Testing, 2005.- [43] K.G. Larsen, M. Mikucionis, B. Nielsen, and A. Skou, "Testing Real-Time Embedded Software Using UPPAAL-TRON—An Industrial Case Study,"
Proc. Fifth ACM Int'l Conf. Embedded Software, Sept. 2005.- [44] L. Carnevali, D. D'Amico, L. Ridi, and E. Vicario, "Automatic Code Generation from Real-Time Systems Specifications,"
Proc. IEEE/IFIP Int'l Symp. Rapid System Prototyping, June 2009.- [45] L. Carnevali, L. Grassi, and E. Vicario, "A Tailored V-Model Exploiting the Theory of Preemptive Time Petri Nets,"
Proc. Ada-Europe Int'l Conf. Reliable Software Technologies, pp. 87-100, 2008.- [46] L. Carnevali, L. Sassoli, and E. Vicario, "Casting Preemptive Time Petri Nets in the Development Life Cycle of Real-Time Software,"
Proc. Euromicro Conf. Real-Time Systems, July 2007.- [47] L. Carnevali, L. Sassoli, and E. Vicario, "Sensitization of Symbolic Runs in Real-Time Testing Using the ORIS Tool,"
Proc. IEEE Conf. Emerging Technologies and Factory Automation, Sept. 2007.- [48] L. Dozio and P. Mantegazza, "General-Purpose Processors for Active Vibro-Acoustic Control: Discussion and Experiences,"
Control Eng. Practice, vol. 15, no. 2, pp. 163-176, Feb. 2007.- [49] L. Sha, R. Rajkumar, and J.P. Lehoczky, "Priority Inheritance Protocols: An Approach to Real-Time Synchronization,"
IEEE Trans. Computers, vol. 39, no. 9, pp. 1175-1185, Sept. 1990.- [50] D. Lime and O.H. Roux, "Formal Verification of Real-Time Systems with Preemptive Scheduling,"
Real-Time Systems, vol. 41, no. 2, pp. 118-151, 2009.- [51] M. Ajmone Marsan, G. Balbo, A. Bobbio, G. Chiola, G. Conte, and A. Cumani, "The Effect of Execution Policies on the Semantics and Analysis of Stochastic Petri Nets,"
IEEE Trans. Software Eng., vol. 15, no. 7, pp. 832-846, July 1989.- [52] M. Krichen and S. Tripakis, "Black-Box Conformance Testing for Real-Time Systems,"
Proc. Int'l SPIN Workshop Model Checking of Software, 2004.- [53] N. Holsti, T. Långbacka, and S. Saarinen,
BoundT Reference Manual, Tidorum Ltd, www.tidorum.fibound-t, 2009.- [54] Object Management Group,
UML Profile for MARTE: Modeling and Analysis of Real-Time Embedded Systems v1.0, 2009.- [55] O.H. Roux and D. Lime, "Time Petri Nets with Inhibitor Hyperarcs: Formal Semantics and State-Space Computation,"
Proc. 25th Int'l Conf. Theory and Application of Petri Nets, vol. 3099, pp. 371-390, 2004.- [56] P. Jordan, "IEC 62304 Int'l Standard Ed. 1.0 Medical Device Software—Software Life Cycle Processes,"
The Institution of Eng. and Technology Seminar on Software for Medical Devices, 2006.- [57] P. Kruchten,
The Rational Unified Process: An Introduction. Addison-Wesley, 2003.- [58] P. Merlin and D.J. Farber, "Recoverability of Communication Protocols,"
IEEE Trans. Comm., vol. 24, no. 9, pp. 1036-1043, Sept. 1976.- [59] R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing, D. Whalley, G. Bernat, C. Ferdinand, R. Heckmann, T. Mitra, F. Mueller, I. Puaut, P. Puschner, J. Statshulat, and P. Stenstroem, "Priority Inheritance Protocols: The Worst Case Execution-Time Problem: Overview of Methods and Survey of Tools,"
ACM Trans. Embedded Computing Systems, vol. 7, no. 3, pp. 1-53, 2008.- [60] Radio Technical Commission for Aeronautics,
DO-178B, Software Considerations in Airborne Systems and Equipment Certification, 1992.- [61] R. Alur, F. Ivancic, J. Kim, I. Lee, and O. Sokolsky, "Generating Embedded Software from Hierarchical Hybrid Models,"
Proc. Languages, Compilers, and Tools for Embedded Systems, pp. 171-182, 2003.- [62] S. Fujiwara, G.V. Bochmann, F. Khendek, M. Amalou, and A. Ghedamsi, "Test Selection Based on Finite-State Models,"
IEEE Trans. Software Eng., vol. 17, no. 6, pp. 591-603, June 1991.- [63] S. Rapps and E.J. Weyuker, "Selecting Software Test Data Using Data Flow Information,"
IEEE Trans. Software Eng., vol. 11, no. 4, pp. 367-375, Apr. 1985.- [64] S.C. Ntafos, "A Comparison of Some Structural Testing Strategies,"
IEEE Trans. Software Eng., vol. 14, no. 6, pp. 868-874, June 1988.- [65] T. Murata, "Petri Nets: Properties, Analysis and Applications,"
Proc. IEEE, vol. 77, no. 4, pp. 541-580, Apr. 1989.- [66] Technische Universität Braunschweig,
Symta/P, www.ida.ing. tu-bs.de/forschung/projekte symtap, 2011.- [67] The Mathworks,
Simulink, www.mathworks.com/products simulink, 2011.- [68] T.A. Henzinger, B. Horowitz, and C.M. Kirsch, "Giotto: A Time-Triggered Language for Embedded Programming,"
Proc. IEEE, vol. 91, no. 1, pp. 84-99, Jan. 2003.- [69] L.-M. Traonouez, D. Lime, and O.H. Roux, "Parametric Model-Checking of Stopwatch Petri Nets,"
J. Universal Computer Science, vol. 15, no. 17, pp. 3273-3304, Dec. 2009.- [70] W. Penczek and A. Polrola, "Specification and Model Checking of Temporal Properties in Time Petri Nets and Timed Automata,"
Proc. Int'l Conf. Application and Theory of Petri Nets, June 2004.- [71] Wind River,
VxWorks, www.windriver.com/productsvxworks, 2011. |