Abstract
Hierarchical Scheduling (HS) systems manage a set of real-time applications through a scheduling hierarchy, enabling partitioning and reduction of complexity, confinement of failure modes, and temporal isolation among system applications. This 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 formal approach to the development of real-time applications with non-deterministic Execution Times and local resource sharing managed by a Time Division Multiplexing (TDM) global scheduler and preemptive Fixed Priority (FP) local schedulers, according to the scheduling hierarchy prescribed by the ARINC-653 standard. The methodology leverages the theory of preemptive Time Petri Nets (pTPNs) to support exact schedulability analysis, to guide the implementation on a Real-Time Operating System (RTOS), and to drive functional conformance testing of the real-time code. Computational experience is reported to show the feasibility of the approach.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
ARINC Specification 653-2: Avionics Application Software Standard Interface: Part 1 - Required Services. Technical report, Avionics Electronic Engineering Committee (ARINC) (March 2006)
Behnam, M., Shin, I., Nolte, T., Nolin, M.: SIRAP: A Synchronization Protocol for Hierarchical Resource Sharing in Real-Time Operating Systems. In: Proc. of the ACM & IEEE Int. Conf. on Embedded SW, pp. 279–288. ACM, New York (2007)
Berthomieu, B., Diaz, M.: Modeling and Verification of Time Dependent Systems Using Time Petri Nets. IEEE Trans. on SW Eng. 17(3) (March 1991)
Bucci, G., Fedeli, A., Sassoli, L., Vicario, E.: Timed State Space Analysis of Real Time Preemptive Systems. IEEE Trans. on SW Eng. 30(2), 97–111 (2004)
Bucci, G., Sassoli, L., Vicario, E.: Correctness verification and performance analysis of real time systems using stochastic preemptive Time Petri Nets. IEEE Trans. on SW Eng. 31(11), 913–927 (2005)
Bucci, G., Vicario, E.: Compositional Validation of Time-Critical Systems Using Communicating Time Petri Nets. IEEE Trans. on SW Eng. 21(12), 969–992 (1995)
Buttazzo, G.: Hard Real-Time Computing Systems. Springer, Heidelberg (2005)
Carnevali, L., Ridi, L., Vicario, E.: Putting preemptive Time Petri Nets to work in a V-Model SW life cycle. IEEE Trans. on SW Eng. (accepted for publication)
Cassez, F., Larsen, K.G.: The Impressive Power of Stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, p. 138. Springer, Heidelberg (2000)
Dill, D.: Timing Assumptions and Verification of Finite-State Concurrent Systems. In: Proc. Workshop on Computer Aided Verification Methods for Finite State Systems (1989)
Davis, R.I., Burns, A.: Hierarchical Fixed Priority Pre-Emptive Scheduling. In: Proc. of the IEEE Int. Real-Time Systems Symp., pp. 389–398 (2005)
Davis, R.I., Burns, A.: Resource Sharing in Hierarchical Fixed Priority Pre-Emptive Systems. In: Proc. IEEE Int. Real-Time Sys. Symp., pp. 257–270 (2006)
Deng, Z., Liu, J.W.-S.: Scheduling real-time applications in an open environment. In: Proc. of the IEEE Real-Time Systems Symp., pp. 308–319 (1997)
Dept. of Aerospace Engineering - Polytechnic of Milan. RTAI: Real Time Application Interface for Linux, https://www.rtai.org
Easwaran, A., Lee, I., Shin, I., Sokolsky, O.: Compositional Schedulability Analysis of Hierarchical Real-Time Systems. In: Proc. of the IEEE Int. Symp. on Object and Component-Oriented Real-Time Distributed Comp., pp. 274–281 (2007)
Easwaran, A., Lee, I., Sokolsky, O., Vestal, S.: A Compositional Scheduling Framework for Digital Avionics Systems. In: Proc. of the Int. Workshop on Real-Time Computing Systems and Applications, vol. 0, pp. 371–380 (2009)
Proctor, F.M., Shackleford, W.P.: Real-time operating system timing jitter and its impact on motor control. In: Proc. of SPIE, Sensors and Controls for Intelligent Manufacturing II, December 10-16, vol. 4563 (2001)
Bucci, G., Carnevali, L., Ridi, L., Vicario, E.: Oris: a Tool for Modeling, Verification and Evaluation of Real-Time Systems. International Journal of Software Tools for Technology Transfer 12(5), 391–403 (2010)
Kuo, T.-W., Li, C.-H.: A Fixed-Priority-Driven Open Environment for Real-Time Applications. In: Proc. IEEE Real-Time Sys. Symp., pp. 256–267 (1999)
Dozio, L., Mantegazza, P.: General-purpose processors for active vibro-acoustic control: Discussion and experiences. Control Engineering Practice 15(2), 163–176 (2007)
Lime, D., Roux, O.H.: Formal verification of real-time systems with preemptive scheduling. Real-Time Syst. 41(2), 118–151 (2009)
Lipari, B.-E., Giuseppe: A methodology for designing hierarchical scheduling systems. Journal of Embedded Computing 1(2), 257–269 (2005)
Lipari, G., Baruah, S.K.: Efficient Scheduling of Real-Time Multi-Task Applications in Dynamic Systems. In: IEEE Real Time Tech. and Appl. Symp., p. 166 (2000)
Lipari, G., Bini, E.: Resource Partitioning among Real-Time Applications. In: Proc. of the Euromicro Conf. on Real-Time Sys., pp. 151–158 (2003)
Merlin, P., Farber, D.: Recoverability of Communication Protocols. IEEE Trans. on Communications 24(9) (1976)
Mok, A.K., Feng, A.X., Chen, D.: Resource Partition for Real-Time Systems. In: IEEE Real Time Technology and Applications Symposium, pp. 75–84 (2001)
Roux, O.H., Lime, D.: Time petri nets with inhibitor hyperarcs. Formal semantics and state space computation. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 371–390. Springer, Heidelberg (2004)
Sha, L., Rajkumar, R., Lehoczky, J.P.: Priority Inheritance Protocols: An Approach to Real-Time Synchronization. IEEE Trans. Comput. 39(9), 1175–1185 (1990)
Shin, I., Lee, I.: Periodic Resource Model for Compositional Real-Time Guarantees. In: Proc. of the IEEE Int. Real-Time Systems Symp., pp. 2–13 (2003)
Spuri, M., Buttazzo, G.: Scheduling Aperiodic Tasks in Dynamic Priority Systems. Real-Time Systems 10, 179–210 (1996)
Vicario, E.: Static Analysis and Dynamic Steering of Time Dependent Systems Using Time Petri Nets. IEEE Trans. on SW Eng. (August 2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Carnevali, L., Lipari, G., Pinzuti, A., Vicario, E. (2011). A Formal Approach to Design and Verification of Two-Level Hierarchical Scheduling Systems. In: Romanovsky, A., Vardanega, T. (eds) Reliable Software Technologies - Ada-Europe 2011. Ada-Europe 2011. Lecture Notes in Computer Science, vol 6652. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21338-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-21338-0_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21337-3
Online ISBN: 978-3-642-21338-0
eBook Packages: Computer ScienceComputer Science (R0)