Abstract
This paper presents a novel flexible, dependable, and reliable operating system design for distributed reconfigurable system on chip. The dependability and reliability are achieved by integrating online model checking technique. Each OS service has different implementations which are further partitioned into small blocks. This operating system design allows the OS service to be adapted at runtime according to the given resource requirements and response time. Such adaptable services may be required by real time safety-critical applications. The flexibility introduced in executing adaptable OS services also gives rise to a potential safety problem. Thus, online model checking is integrated to the operating system so as to improve the dependability, reliability, and fault tolerance of these adaptable OS services.
Chapter PDF
Similar content being viewed by others
References
Samara, S., Tariq, F.B., Kerstan, T., Stahl, K.: Applications adaptable execution path for operating system services on a distributed reconfigurable system on chip. In: ICESS 2009: Proceedings of the 2009 International Conference on Embedded Software and Systems, Washington, DC, USA, pp. 461–466. IEEE Computer Society, Washington (2009)
Samara, S., Schomaker, G.: Self-adaptive os service model in relaxed resource distributed reconfigurable system on chip (rsoc). In: Proceedings of the 2009 Computation World: Future Computing, Service Computation, Cognitive, Adaptive, Content, Patterns, Washington, DC, USA, pp. 1–8. IEEE Computer Society, Washington (2009)
Zhao, Y., Rammig, F.J.: Model-based runtime verification framework. Electronic Notes in Theoretical Computer Science 253(1), 179–193 (2009)
Rammig, F.J., Zhao, Y., Samara, S.: On-line model checking as operating system service. In: Lee, S., Narasimhan, P. (eds.) SEUS 2009. LNCS, vol. 5860, pp. 131–143. Springer, Heidelberg (2009)
Graf, S., Saidi, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Engel, F., Kuz, I., Petters, S.M., Ruocco, S.: Operating systems on socs: A good idea? National ICT Australia Ltd. (2004)
Wigley, G., Kearney, D.: Research issues in operating systems for reconfigurable computing. In: Proceedings of the International Conference on Engineering of Reconfigurable System and Algorithms (ERSA), pp. 10–16. CSREA Press (2002)
Donato, A., Ferrandi, F., Santamberogio, M., Sciuto, D.: Operating system support for dynamically reconfigurable soc. architectures. Politecnico di Milano (2006)
Nollet, V., Coene, P., Verkest, D., Vernalde, S., Lauwereins, R.: Designing an operating system for a heterogeneous reconfigurable soc. In: Proceedings of the RAW 2003 workshop (2003)
Walder, H., Platzner, M.: A runtime environment for reconfigurable hardware operating systems. In: Becker, J., Platzner, M., Vernalde, S. (eds.) FPL 2004. LNCS, vol. 3203, pp. 831–835. Springer, Heidelberg (2004)
Götz, M., Rettberg, A., Pereira, C.E.: Run-time reconfigurable real-time operating system for hybrid execution platforms. In: Information Control Problems in Manufacturing, IFAC (2006)
Götz, M., Rettberg, A., Pereira, C.E.: Towards run-time partitioning of a real time operating system for reconfigurable systems on chip. In: IFIP International Federation for Information Processing (2005)
Gajski, D.D., Vahid, F.: Specification and design of embedded hardware-software systems. IEEE, Design & Test of Computers 12, 53–67 (1995)
Clark, E.M., Grumberg Jr., O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, Secaucus, NJ, USA. Springer, New York (1996), Foreword By-Wolper, Pierre
Berezin, S., Campos, S.V.A., Clarke, E.M.: Compositional reasoning in model checking. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 81–102. Springer, Heidelberg (1998)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)
Lee, W., Pardo, A., Jang, J.Y., Hachtel, G., Somenzi, F.: Tearing based automatic abstraction for ctl model checking. In: ICCAD 1996: Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, Washington, DC, USA, pp. 76–81. IEEE Computer Society, Los Alamitos (1996)
Barnett, M., Schulte, W.: Spying on components: A runtime verification technique. In: Leavens, G.T., Sitaraman, M., Giannakopoulou, D., eds.: Workshop on Specification and Verification of Component-Based Systems. October 2001, Published as Iowa State Technical Report 01-09a (October 2001)
Arkoudas, K., Rinard, M.: Deductive Runtime Certification. In: Proceedings of the 2004 Workshop on Runtime Verification (RV 2004), Barcelona, Spain (April 2004)
Chen, F., Rosu, G.: Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation. In: Proceedings of the 2003 Workshop on Runtime Verification (RV 2003), Boulder, Colorado, USA (2003)
Havelund, K., Rosu, G.: Java PathExplorer — a runtime verification tool. In: Proceedings 6th International Symposium on Artificial Intelligence, Robotics and Automation in Space (ISAIRAS 2001), Montreal, Canada (June 2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 IFIP
About this paper
Cite this paper
Samara, S., Zhao, Y., Rammig, F.J. (2010). Integrate Online Model Checking into Distributed Reconfigurable System on Chip with Adaptable OS Services. In: Hinchey, M., et al. Distributed, Parallel and Biologically Inspired Systems. DIPES BICC 2010 2010. IFIP Advances in Information and Communication Technology, vol 329. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15234-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-15234-4_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15233-7
Online ISBN: 978-3-642-15234-4
eBook Packages: Computer ScienceComputer Science (R0)