Abstract
Architecture Description Languages (ADLs) allow embedded systems to be described as assemblies of hardware and software components. It is attractive to use such a global modelling as a basis for early system analysis. However, in such descriptions, the applicative software is often abstracted away, and is supposed to be developed in some host programming language. This forbids to take the applicative software into account in such early validation. To overcome this limitation, a solution consists in translating the ADL description into an executable model, which can be simulated and validated together with the software. In a previous paper [1], we proposed such a translation of Aadl (Architecture Analysis & Design Language) specifications into an executable synchronous model.
The present paper is a continuation of this work, and deals with expressing the behavior of complex scheduling policies managing shared resources. We provide a synchronous specification for two shared resource scheduling protocols: the well-known basic priority inheritance protocol (BIP), and the priority ceiling protocol (PCP). This results in an automated translation of Aadl models into a purely Boolean synchronous (Lustre) scheduler, that can be directly model-checked, possibly with the actual software.
This work was partially supported by the European Commission under the Integrated Project ASSERT, IST 004033, which ended in 2008.
Chapter PDF
Similar content being viewed by others
Keywords
References
Halbwachs, N., Jahier, E., Raymond, P., Nicollin, X., Lesens, D.: Virtual execution of AADL models via a translation into synchronous programs. In: Seventh International Conference on Embedded Software (EMSOFT 2007), Salzburg, Austria (October 2007)
Feiler, P.H., Gluch, D.P., Hudak, J.J., Lewis, B.A.: Embedded system architecture analysis using SAE AADL. Technical note cmu/sei-2004-tn-005, Carnegie Mellon University (2004)
SAE: Architecture Analysis & Design Language (AADL). AS5506, Version 1.0, SAE Aerospace (November 2004)
Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language Lustre. Proceedings of the IEEE 79(9), 1305–1320 (1991)
Liu, C.L., Layland, J.: Scheduling algorithms for multiprogramming in a hard real-time environment. JACM 20(1), 46–61 (1973)
Milner, R.: On relating synchrony and asynchrony. Technical Report CSR-75-80, Computer Science Dept., Edimburgh Univ. (1981)
Baufreton, P.: SACRES: A step ahead in the development of critical avionics applications. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, p. 1. Springer, Heidelberg (1999)
Baufreton, P.: Visual notations based on synchronous languages for dynamic validation of gals systems. In: CCCT 2004 Computing, Communications and Control Technologies, Austin (Texas) (August 2004)
Gamatié, A., Gautier, T.: Synchronous modeling of avionics applications using the signal language. In: 9th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2003), Toronto, pp. 144–151 (May 2003)
Gamatié, A., Gautier, T.: The signal approach to the design of system architectures. In: 10th IEEE Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2003), Huntsville (Alabama), pp. 80–88 (April 2003)
Le Guernic, P., Talpin, J.P., Le Lann, J.C.: Polychrony for system design. Journal for Circuits, Systems and Computers, Special Issue on Application Specific Hardware Design (April 2003)
Sha, L., Rajkumar, R., Lehoczky, J.P.: Priority inheritance protocols: An approach to real-time synchronization. IEEE Trans. Computers 39(9), 1175–1185 (1990)
Halbwachs, N., Lagnier, F., Ratel, C.: Programming and verifying real-time systems by means of the synchronous data-flow programming language Lustre. IEEE Transactions on Software Engineering, Special Issue on the Specification and Analysis of Real-Time Systems, 785–793 (September 1992)
Hugues, J., Zalila, B., Kordon, L.P.F.: Rapid prototyping of distributed real-time embedded systems using the AADL and Ocarina. In: 18th IEEE/IFIP International Workshop on Rapid System Prototyping (RSP 2007) (2007)
Singhoff, F., Legrand, J., Nana, L., Marcé, L.: Cheddar: a flexible real time scheduling framework. In: McCormick, J.W., Sward, R.E. (eds.) SIGAda, pp. 1–8. ACM, New York (2004)
Singhoff, F., Legrand, J., Nana, L., Marcé, L.: Scheduling and memory requirements analysis with AADL. In: SIGAda (2005)
Guernic, P.L., Benveniste, A., Bournai, P., Gautier, T.: Signal, a data flow oriented language for signal processing. IEEE-ASSP 34(2), 362–374 (1986)
Dutertre, B.: Formal analysis of the priority ceiling protocol. In: IEEE Real-Time Systems Symposium (RTSS 2000), pp. 151–160 (2000)
Penix, J., Visser, W., Engstrom, E., Larson, A., Weininger, N.: Verification of time partitioning in the deos scheduler kernel. In: ICSE, pp. 488–497 (2000)
Jahier, E., Raymond, P., Baufreton, P.: Case studies with Lurette V2. International Journal on Software Tools for Technology Transfer (STTT) Special Section on Leveraging Applications of Formal Methods (2006)
Raymond, P., Jahier, E., Roux, Y.: Describing and executing random reactive systems. In: SEFM, pp. 216–225. IEEE Computer Society, Los Alamitos (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jahier, E., Halbwachs, N., Raymond, P. (2009). Synchronous Modeling and Validation of Priority Inheritance Schedulers. In: Chechik, M., Wirsing, M. (eds) Fundamental Approaches to Software Engineering. FASE 2009. Lecture Notes in Computer Science, vol 5503. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00593-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-00593-0_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00592-3
Online ISBN: 978-3-642-00593-0
eBook Packages: Computer ScienceComputer Science (R0)