Rasmus Adler
Skip Abstract Section
Abstract
Adaptation is increasingly used in the development of safety-critical embedded systems, in particular to reduce hardware needs and to increase availability. However, composing a system from many reconfigurable components can lead to a huge number of possible system configurations, inducing a complexity that cannot be handled during system design. To overcome this problem, we propose a new component-based modeling and verification method for adaptive embedded systems. The component-based modeling approach facilitates abstracting a composition of components to a hierarchical component. In the hierarchical component, the number of possible configurations of the composition is reduced to a small number of hierarchical configurations. Only these hierarchical configurations have to be considered when the hierarchical component is used in further compositions such that design complexity is reduced at each hierarchical level. In order to ensure well-definedness of components, we provide a model of computation enabling the formal verification of critical requirements of the adaptation behavior.
- Adler, R., Schaefer, I., Schuele, T., and Vecchie, E. 2007. From model-based design to formal verification of adaptive embedded systems. In Proceedings of the International Conference on Formal Engineering Methods. IEEE, Los Alamitos, CA. Google Scholar
Digital Library
- Agha, G. 1986. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, MA. Google ScholarCross Ref
- Atkinson, C., Bayer, J., Bunse, C., Kamsties, E., Laitenberger, O., Laqua, R., Muthig, D., Paech, B., Wust, J., and Zettel, J. 2002. Component-Based Product Line Engineering with UML. Addison-Wesley, Upper Saddle River, NJ. Google ScholarDigital Library
- Basu, A., Bozga, M., and Sifakis, J. 2006. Modeling heterogeneous real-time components in BIP. In Proceedings of the International Conference on Software Engineering and Formal Methods. IEEE, Los Alamitos, CA, 3--12. Google ScholarDigital Library
- Benveniste, A., Caspi, P., Edwards, S., Halbwachs, N., Le Guernic, P., and de Simone, R. 2003. The synchronous languages twelve years later. Proc. IEEE 91, 1.Google ScholarCross Ref
- Bures, T., Hnetynka, P., and Plasil, F. 2006. SOFA 2.0: Balancing advanced features in a hierarchical component model. In Proceedings of the International Conference on Software Engineering Research, Management and Applications. IEEE, Los Alamitos, CA. Google ScholarDigital Library
- Burmester, S., Giese, H., Hirsch, M., Schilling, D., and Tichy, M. 2005. The Fujaba real-time tool suite: Model-driven development of safety-critical, real-time systems. In Proceedings of the International Conference on Software Engineering. IEEE, Los Alamitos, CA. Google ScholarDigital Library
- Clarke, E., Grumberg, O., and Peled, D. 1999. Model checking. MIT Press. Google ScholarDigital Library
- Damm, W., Votintseva, A., Metzner, A., Josko, B., Peikenkamp, T., and Bõde, E. 2005. Boosting re-use of embedded automotive applications through rich components. In Proceedings of the Foundations of Interface Technologies. Elsevier Science, Burlington, MA.Google Scholar
- de Alfaro, L. and Henzinger, T. A. 2001. Interface automata. In Proceedings of the Symposium on Foundations of Software Engineering. ACM, New York, 109--120. Google ScholarDigital Library
- Eker, J., Janneck, J. W., Lee, E. A., Liu, J., Liu, X., Ludvig, J., Neuendorffer, S., Sachs, S., and Xiong, Y. 2003. Taming heterogeneity—the Ptolemy approach. Proc. IEEE. 91, 1, 127--144.Google ScholarCross Ref
- Geilen, M. and Basten, T. 2004. Reactive process networks. In Proceedings of the International Conference on Embedded Software. ACM, New York. Google ScholarDigital Library
- Gjørven, E., Eliassen, F., and Rouvoy, R. 2008. Experiences from developing a component technology agnostic adaptation framework. In Proceedings of the International Conference on Component Based Software Engineering. Google ScholarDigital Library
- Harel, D. 1987. A visual formalism for complex systems. Sci. Comput. Program. 8, 3, 231--274. Google ScholarDigital Library
- Hnetynka, P. and Bures, T. 2007. Advanced features of hierarchical component models. In Proceedings of the International Conference on Information System Implementation and Modeling.Google Scholar
- Jantsch, A. 2004. Modeling Embedded Systems and SoCs. Morgan Kaufmann, San Francisco, CA. Google ScholarDigital Library
- Kemman, S. 2007. Tool supported specification of embedded component systems. Internal rep. Department of Component Engineering, Fraunhofer IESE.Google Scholar
- Ledeczi, A., Maroti, M., Bakay, A., Karsai, G., Garrett, J., Thomason, C., Nordstrom, G., Sprinkle, J., and Volgyesi, P. 2001. The generic modeling environment. In Proceedings of the Workshop on Intelligent Signal Processing. IEEE, Los Alamitos, CA.Google Scholar
- Lee, E. A. and Xiong, Y. 2004. A behavioral type system and its application in Ptolemy II. Formal Aspects Comput. 16, 3. Google ScholarCross Ref
- Lyu, M. R. 1995. Software Fault Tolerance. John Wiley and Sons, New York. Google ScholarDigital Library
- Manna, Z. and Pnueli, A. 1995. Temporal Verification of Reactive Systems: Safety. Springer, Berlin. Google ScholarDigital Library
- Mousavi, M. R., Reniers, M., Basten, T., and Chaudron, M. 2003. Separation of concerns in the formal design of real-time shared data-space systems. In Proceedings of the International Conference on Application of Concurrency to System Design. IEEE, Los Alamitos, CA. Google ScholarDigital Library
- Nipkow, T., Paulson, L., and Wenzel, M. 2002. Isabelle/HOL—A proof Assistant for Higher-Order Logic. Springer, Berlin. Google ScholarDigital Library
- Plasil, F. and Visnovsky, S. 2002. Behavior protocols for software components. IEEE Trans. Software Eng. 28, 11. Google ScholarDigital Library
- Rawashdeh, O. and Lumpp, J.E., J. 2006. Run-time behavior of Ardea: A dynamically reconfigurable distributed embedded control architecture. Proceedings of the Aerospace Conference. IEEE, Los Alamitos, CA.Google Scholar
- Schaefer, I. 2008. Integrating formal verification into the model-based development for adaptive embedded systems. Ph.D. thesis, University of Kaiserslautern.Google Scholar
- Schneider, K. and Schuele, T. 2005. Averest: Specification, verification, and implementation of reactive systems. In Proceedings of the International Conference on Application of Concurrency to System Design. IEEE, Los Alamitos, CA.Google Scholar
- Schneider, K., Schuele, T., and Trapp, M. 2006. Verifying the adaptation behavior of embedded Systems. In Proceedings of the International Workshop on Software Engineering for Adaptive and Self-Managing Systems. IEEE, Los Alamitos, CA. Google ScholarDigital Library
- Selic, B., Gullekson, G., and Ward, P. T. 1994. Real-Time Object-Oriented Modeling. John Wiley and Sons, New York. Google ScholarDigital Library
- Shelton, C. P. 2003. A framework for scalable analysis and design of system-wide graceful degradation in distributed embedded systems. In Proceedings of the International Workshop on Object-Oriented Real-Time Dependable Systems. IEEE, Los Alamitos, CA.Google ScholarCross Ref
- Shelton, C. P. and Koopman, P. 2004. Improving system dependability with functional alternatives. In Proceedings of the International Conference on Dependable Systems and Networks. IEEE, Los Alamitos, CA. Google ScholarDigital Library
- Strunk, E. A. and Knight, J. C. 2006. Dependability through assured reconfiguration in embedded system software. IEEE Trans. Depend, Secure Comput. 3, 3. Google ScholarDigital Library
- Szyperski, C. 1999. Component Software. Beyond Object-Oriented Programming. ACM, New York. Google ScholarDigital Library
- Trapp, M. 2005. Modeling the adaptation behavior of adaptive embedded systems. Ph.D. thesis, University of Kaiserslautern.Google Scholar
- Trapp, M., Adler, R., Förster, M., and Junger, J. 2007. Runtime adaptation in safety-critical automotive systems. In Proceedings of the International Multi-Conference on Software Engineering. Google ScholarDigital Library
- Vallée, M., Ramparany, F., and Vercouter, L. 2005. Dynamic service composition in ambient intelligence environments: A multi-agent approach. In Proceedings of the 1st European Young Researcher Workshop on Service-Oriented Computing.Google Scholar
- van Ommering, R. C. 1998. Koala, a component model for consumer electronics product software. In Proceedings of the Workshop on Development and Evolution of Software Architectures for Product Families. Google ScholarDigital Library
- Yan, Z., Prehofer, C., and Niemi, V. 2007. Trust4All: A trustworthy middleware platform for component software. In Proceedings of the International Conference on Applied Informatics and Communications. Google ScholarDigital Library
- Zhang, J. and Cheng, B. 2006. Model-based development of dynamically adaptive software. In Proceedings of the International Conference on Software Engineering. IEEE, Los Alamitos, CA, 371--380. Google ScholarDigital Library
Index Terms
- Component-based modeling and verification of dynamic adaptation in safety-critical embedded systems
Recommendations
Automatic Composition of AADL Models for the Verification of Critical Component-Based Embedded Systems
ICECCS '08: Proceedings of the 13th IEEE International Conference on on Engineering of Complex Computer SystemsEarly analysis and verification of a critical embedded system requires a precise platform specific model (PSM) of the whole system. On the other hand, to master the complexity of large complex critical distributed real-time and embedded systems (DRES), ...
A Component-Based Approach to Hybrid Systems Safety Verification
IFM 2016: Proceedings of the 12th International Conference on Integrated Formal Methods - Volume 9681We study a component-based approach to simplify the challenges of verifying large-scale hybrid systems. Component-based modeling can be used to split large models into partial models to reduce modeling complexity. Yet, verification results also need to ...
Modelling and Verification of Port Based Component Composition
QSIC '09: Proceedings of the 2009 Ninth International Conference on Quality SoftwareThis paper presents a port based language to describe components and component composition. This language aims to check component composition in three aspects: signature constraints, behaviour compatibility and run time errors. For the run time errors, ...
Comments