Handling mixed-criticality in SoC-based real-time embedded systems

ABSTRACT

System-on-Chip (SoC) is a promising paradigm to implement safety-critical embedded systems, but it poses significant challenges from a design and verification point of view. In particular, in a mixed-criticality system, low criticality applications must be prevented from interfering with high criticality ones. In this paper, we introduce a new design methodology for SoC that provides strong isolation guarantees to applications with different criticalities. A set of certificates describing the assumed application behavior is extracted from a functional Architectural Analysis and Design Language (AADL) specification. Our tools then automatically generate hardware wrappers that enforce at run-time the behavior described by the certificates. In particular, we employ run-time monitoring to formally check all data communication in the system, and we enforce timing reservations for both computation and communication resources. Verification is greatly simplified because certificates are much simpler than the components used to implement low-criticality applications. The effectiveness of our methodology is proven on a case study consisting of a medical pacemaker.

REFERENCES

• 1: Aeronautical Radio Inc. ARINC 653 Specification. http://www.arinc.com/.
• 2: B. Akesson, K. Goossens, and M. Ringhofer. Predator: a predictable sdram memory controller. In Proc. of the 5th IEEE/ACM inter. conference on HW/SW codesign and system synthesis, 2007.
• 3: P. Avgustinov, J. Tibble, and O. de Moor. Making trace monitors feasible. In Proc. of the ACM Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'07), pages 589--608, 2007.
• 4: S. Bak, D. Chivukula, O. Adekunle, M. Sun, M. Caccamo, and L. Sha. The system-level simplex architecture for improved real-time embedded system safety. In Proceedings of the IEEE RTAS, 2009.
• 5: H. Barringer, A. Goldberg, K. Havelund, and K. Sen. Rule-based runtime verification. In Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'04), pages 277--306, 2004.
• 6: Pam Binns, Matt Englehart, Mike Jackson, and Steve Vestal. Domain Specific Software Architectures for Guidance, Navigation and Control. International Journal of Software Engineering and Knowledge Engineering, 6(2):201--227, 1996.
• 7: M. Caccamo, L. Y. Zhang, L. Sha, and G. Buttazzo. An implicit prioritized access protocol for wireless sensor networks. In Proceedings of the IEEE RTSS, Dec 2002.
• 8: F. Chen and G. Roşu. MOP: An Efficient and Generic Runtime Verification Framework. In Proc. of the ACM OOPSLA, pages 569--588, 2007.
• 9: T. Chen, R. Raghavan, J. Dale, and E. Iwata. Cell broadband engine architecture and its first implementation: A performance view. Technical report, IBM Research, 2005.
• 10: P. Cumming. The TI OMAP platform approach to SoCs. In Surviving the SoC revolution: A guide to platform-based design. Kluwer, 1999.
• 11: E.A. Emerson. Handbook of Theoretical Computer Science. MIT Press, 1990. Chapter 16: Temporal and modal logic.
• 12: F. Balarin et al. Metropolis: An integrated electronic system design environment. IEEE Computers, 36(4):45--52, 2003.
• 13: M. Clavel et al. The maude 2.0 system. In Proc. Rewriting Techniques and Applications, 2003.
• 14: P.H. Feiler, B.A. Lewis, and S. Vestal. The SAE Architecture Analysis & Design Language (AADL): A Standard for Engineering Performance Critical Systems. In Proc, of the 2006 IEEE Conference on Computer Aided Control Systems Design, Oct. 2006.
• 15: K. Goossens, J. Dielissen, and A. Radulescu. othereal network on chip: Concepts, architectures, and implementations. IEEE Design and Test, 22(5):414--421, 2005.
• 16: K. Havelund and G. Rosu. Monitoring Java programs with Java pathexplorer. In Proc. First Workshop on Runtime Verification, 2001.
• 17: J. Hugues, B. Zalila, L. Pautet, and F. Kordon. From the prototype to the final embedded system using the Ocarina AADL tool suite. ACM Trans. on Emb. Computing Sys., 7(4):1--25, 2008.
• 18: IBM. Processor Local Bus Specification. http://www-01.ibm.com/chips/techlib/techlib.nsf/techdocs/3BBB27E5BCC165BA87256A2B0064FFB4.
• 19: G. Karsai, J. Sztipanovits, A. Ledeczi, and T. Bapty. Model-integrated development of embedded software. Proceedings of the IEEE, 91(1):145--164, 2003.
• 20: M. Kim, M. Viswanathan, S. Kannan, I. Lee, and O. Sokolsky. Java-mac: A run-time assurance approach for Java programs. Formal Methods in System Design, 24(2):129--155, 2004.
• 21: D. Knuth. Backus normal form vs. backus naur form. Communications of the ACM, 7(12):735--736, 1964.
• 22: B. Lickly, I. Liu, S. Kim, H. Patel, S. Edwards, and E. Lee. Predictable programming on a precision timed architecture. In Proceedings of International Conference on Compilers, Architecture, and Synthesis from Embedded Systems, Oct 2008.
• 23: H. Lu and A. Forin. The design and implementation of p2v, an architecture for zero-overhead online verification of software programs. Technical Report MSR-TR-2007-99, Microsoft Research, 2007.
• 24: M. Sipser. Introduction to the Theory of Computation. PWS Publishing, 1996. Chapter 1: Regular Languages.
• 25: M. Martin, B. Livshits, and M. Lam. Finding application errors and security flaws using PQL: a program query language. In Proc. of the ACM Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'05), pages 365--383, 2005.
• 26: NXP Semiconductors. Philips Nexperia Digital Video Platform. http://www.nxp.com.
• 27: R. Pellizzoni, P. Meredith, M. Caccamo, and G. Rosu. Hardware runtime monitoring for dependable COTS-based real-time embedded systems. In Proceedings of the 29th IEEE RTSS, Dec 2008.
• 28: A.-E. Rugina, K. Kanoun, and M. Kaaniche. The ADAPT Tool: From AADL Architectural Models to Stochastic Petri Nets through Model Transformation. In Dependable Computing Conference, 2008. EDCC 2008. Seventh European, pages 85--90, May 2008.
• 29: A. Sangiovanni-Vincentelli. Quo vadis, SLD? reasoning about the trends and challenges of system level design. Proceedings of the IEEE, 95(3):467--506, 2007.
• 30: F. Singhoff, J. Legrand, L. Nana, and L. Marce. Scheduling and memory requirements analysis with AADL. In Proceedings of ACM SIGAda, volume 25, pages 1--10, Atlanta, Georgia, 2005.
• 31: O. Sokolsky, I. Lee, and D. Clarke. Schedulability analysis of AADL models. Parallel and Distributed Processing Symposium, 2006. IPDPS 2006. 20th International, April 2006.
• 32: H. Sun, M. Hauptman, and R. Lutz. Integrating product-line fault tree analysis into aadl models. In High Assurance Systems Engineering Symposium, 2007. HASE '07. 10th IEEE, pages 15--22, 2007.
• 33: University of Illinois. HW-SW Architectures for SoC-based Real-Time Embedded Systems. http://pertsserver.cs.uiuc.edu/~fpgaweb.
• 34: Uppsala University and Aalborg Univeristy. Uppaal a tool suite for verification of real-time systems. www.uppaal.com.
• 35: John G. Webster. Cardiac Pacemakers. IEEE Press, 1993.
• 36: Xilinx, Inc. Virtex-5 User Guide. Available at www.xilinx.com.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.4 INPUT/OUTPUT AND DATA COMMUNICATIONS
      B.4.3 Interconnections (subsystems)

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques

General Terms:
Design, Reliability, Verification

Keywords:
AADL, mixed-criticality, platform-based design, runtime monitoring, system-on-chip