The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.05 - May (2013 vol.39)
pp: 638-657
Laura Carnevali , Università di Firenze
Alessandro Pinzuti , Università di Firenze
Enrico Vicario , Università di Firenze
ABSTRACT
Hierarchical Scheduling (HS) techniques achieve resource partitioning among a set of real-time applications, providing reduction of complexity, confinement of failure modes, and temporal isolation among system applications. This facilitates compositional analysis for architectural verification and plays a crucial role in all industrial areas where high-performance microprocessors allow growing integration of multiple applications on a single platform. We propose a compositional approach to formal specification and schedulability analysis of real-time applications running under a Time Division Multiplexing (TDM) global scheduler and preemptive Fixed Priority (FP) local schedulers, according to the ARINC-653 standard. As a characterizing trait, each application is made of periodic, sporadic, and jittering tasks with offsets, jitters, and nondeterministic execution times, encompassing intra-application synchronizations through semaphores and mailboxes and interapplication communications among periodic tasks through message passing. The approach leverages the assumption of a TDM partitioning to enable compositional design and analysis based on the model of preemptive Time Petri Nets (pTPNs), which is expressly extended with a concept of Required Interface (RI) that specifies the embedding environment of an application through sequencing and timing constraints. This enables exact verification of intra-application constraints and approximate but safe verification of interapplication constraints. Experimentation illustrates results and validates their applicability on two challenging workloads in the field of safety-critical avionic systems.
INDEX TERMS
Real time systems, Complexity theory, Time division multiplexing, Job shop scheduling, Timing, Resource management, Petri nets, symbolic state-space analysis, Real-time systems, hierarchical scheduling, ARINC-653, time division multiplexing, preemptive fixed priority, compositional verification, preemptive time Petri nets
CITATION
Laura Carnevali, Alessandro Pinzuti, Enrico Vicario, "Compositional Verification for Hierarchical Scheduling of Real-Time Systems", IEEE Transactions on Software Engineering, vol.39, no. 5, pp. 638-657, May 2013, doi:10.1109/TSE.2012.54
REFERENCES
[1] Avionics Application Software Standard Interface: Part 1—Required Services (ARINC Specification 653-2), technical report, Avionics Electronic Eng. Committee (ARINC), Mar. 2006.
[2] M. Behnam, I. Shin, T. Nolte, and M. Nolin, "SIRAP: A Synchronization Protocol for Hierarchical Resource Sharing Real-Time Open Systems," Proc. ACM/IEEE Seveth Int'l Conf. Embedded Software, pp. 279-288, 2007.
[3] 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.
[4] B. Berthomieu, D. Lime, O.H. Roux, and F. Vernadat, "Reachability Problems and Abstract State Spaces for Time Petri Nets with Stopwatches," Discrete Event Dynamic Systems, vol. 17, no. 2, pp. 133-158, June 2007.
[5] B. Berthomieu and M. Menasche, "An Enumerative Approach for Analyzing Time Petri Nets," Proc. IFIP Ninth World Congress, R.E.A. Mason, ed., vol. 9, pp. 41-46, 1983.
[6] I. Bicchierai, G. Bucci, L. Carnevali, and E. Vicario, "Combining UML-MARTE and Preemptive Time Petri Nets: An Industrial Case Study," IEEE Trans. Industrial Informatics, accepted for publication.
[7] E. Bini and G. Buttazzo, "A Hyperbolic Bound for Rate Monotonic Algorithm," Proc. 13th Euromicro Conf. Real-Time Systems, 2001.
[8] 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.
[9] 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.
[10] G. Bucci and E. Vicario, "Compositional Validation of Time-Critical Systems Using Communicating Time Petri Nets," IEEE Trans. Software Eng., vol. 21, no. 12, pp. 969-992, Nov.Dec. 1995.
[11] G. Buttazzo, Hard Real-Time Computing Systems. Springer, 2005.
[12] L. Carnevali, G. Lipari, A. Pinzuti, and E. Vicario, "A Formal Approach to Design and Verification of Two-Level Hierarchical Scheduling Systems," Proc. Ada-Europe Int'l Conf. Reliable Software Technologies, pp. 118-131, 2011.
[13] L. Carnevali, L. Ridi, and E. Vicario, "Putting Preemptive Time Petri Nets to Work in a V-Model SW Life Cycle," IEEE Trans. Software Eng., vol. 37, no. 6, pp. 826-844, Nov./Dec. 2011.
[14] F. Cassez and K.G. Larsen, "The Impressive Power of Stopwatches," Proc. 11th Int'l Conf. Concurrency Theory, Aug. 2000.
[15] D. Dill, "Timing Assumptions and Verification of Finite-State Concurrent Systems," Proc. Int'l Workshop Automatic Verification Methods for Finite State Systems, vol. 407, 1990.
[16] R.I. Davis and A. Burns, "Hierarchical Fixed Priority Pre-Emptive Scheduling," Proc. 26th IEEE Int'l Real-Time Systems Symp., pp. 389-398, 2005.
[17] R.I. Davis and A. Burns, "Resource Sharing in Hierarchical Fixed Priority Pre-Emptive Systems," Proc. 27th IEEE Int'l Real-Time Systems Symp., pp. 257-270, 2006.
[18] Z. Deng and J.W. Liu, "Scheduling Real-Time Applications in an Open Environment," Proc. 18th IEEE Real-Time Systems Symp., pp. 308-319, 1997.
[19] R.B. Dodd, "An Analysis of task Scheduling for a Generic Avionics Mission Computer," technical report, Australian Govt., Dept. of Defence, Defence Science and Technology Organisation, Oct. 2006.
[20] R.B. Dodd, "Coloured Petri Net Modelling of a Generic Avionics Mission Computer," technical report, Australian Govt., Dept. of Defence, Defence Science and Technology Organisation, Apr. 2006.
[21] A. Easwaran, M. Anand, and I. Lee, "Compositional Analysis Framework Using EDP Resource Models," Proc. 28th IEEE Int'l Real-Time Systems Symp., pp. 129-138, 2007.
[22] A. Easwaran, I. Lee, I. Shin, and O. Sokolsky, "Compositional Schedulability Analysis of Hierarchical Real-Time Systems," Proc. 10th IEEE Int'l Symp. Object and Component-Oriented Real-Time Distributed Computing, pp. 274-281, 2007.
[23] A. Easwaran, I. Lee, O. Sokolsky, and S. Vestal, "A Compositional Scheduling Framework for Digital Avionics Systems," Proc. Int'l Workshop Real-Time Computing Systems and Applications, pp. 371-380, 2009.
[24] X.A. Feng and A.K. Mok, "A Model of Hierarchical Real-Time Virtual Resources," Proc. 23rd IEEE Real-Time Systems Symp., pp. 26-35, 2002.
[25] 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.
[26] G. Gardey, D. Lime, M. Magnin, and O.(H.) Roux, "Roméo: A Tool for Analyzing Time Petri Nets," Computer Aided Verification, Springer, 2005.
[27] T.W. Kuo and C.H. Li, "A Fixed-Priority-Driven Open Environment for Real-Time Applications," Proc. Real-Time Systems Symp., pp. 256-267, 1999.
[28] 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.
[29] G. Lipari and S.K. Baruah, "Efficient Scheduling of Real-Time Multi-Task Applications in Dynamic Systems," Proc. IEEE Real Time Technology and Applications Symp., pp. 166-175, 2000.
[30] G. Lipari and E. Bini, "Resource Partitioning among Real-Time Applications," Proc. Euromicro Conf. Real-Time Systems, pp. 151-158, 2003.
[31] G. Lipari and E. Bini, "A Methodology for Designing Hierarchical Scheduling Systems," J. Embedded Computing, vol. 1, no. 2, pp. 257-269, 2005.
[32] C.D. Locke, D.R. Vogel, and L. Lucas, "Generic Avionics Software Specification," technical report, Software Eng. Inst., Carnegie Mellon Univ., 1990.
[33] A.K. Mok, A.X. Feng, and D. Chen, "Resource Partition for Real-Time Systems," Proc. IEEE Real Time Technology and Applications Symp., pp. 75-84, 2001.
[34] Object Management Group., UML Profile for MARTE: Modeling and Analysis of Real-Time Embedded Systems v1.0, 2009.
[35] 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, pp. 371-390, 2004.
[36] L. Sassoli and E. Vicario, "Analysis of Real Time Systems through the Oris Tool," Proc. Third Int'l Conf. Quantitative Evaluation of Systems, Sept. 2006.
[37] 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.
[38] I. Shin and I. Lee, "Periodic Resource Model for Compositional Real-Time Guarantees," Proc. IEEE 24th Int'l Real-Time Systems Symp., pp. 2-13, 2003.
[39] M. Spuri and G. Buttazzo, "Scheduling Aperiodic Tasks in Dynamic Priority Systems," Real-Time Systems, vol. 10, pp. 179-210, 1996.
[40] 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.
[41] E. Vicario, "Static Analysis and Dynamic Steering of Time Dependent Systems Using Time Petri Nets," IEEE Trans. Software Eng., vol. 27, no. 8, pp. 728-748, Aug. 2001.
6 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool