Abstract
Ambient Intelligence systems integrate domotic devices and advanced control and intelligent algorithms, thus leading to integrate systems with a high degree of complexity in their behavior. Ensuring the correctness of the design of such system is therefore essential, and this paper proposed a methodology, based on formal modeling and verification techniques, to verify logic and temporal properties of an intelligent ambient. The approach is integrated with the Dog domotic gateway, and automatic translation tools ensure the correctness of the verified model while adding no additional task for system designers.
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.
References
Augusto, J.C., Mccullagh, P.: Ambient Intelligence: Concepts and Applications. Computer Science and Information Systems 4(1), 1–27 (2007)
Bonino, D., Castellina, E., Corno, F.: The DOG gateway: Enabling Ontology-based Intelligent Domotic Environments. IEEE Transactions on Consumer Electronics 54(4), 1656–1664 (2008), doi:10.1109/TCE.2008.4711217
Bonino, D., Corno, F.: DogOnt - ontology modeling for intelligent domotic environments. In: Sheth, A.P., Staab, S., Dean, M., Paolucci, M., Maynard, D., Finin, T., Thirunarayan, K. (eds.) ISWC 2008. LNCS, vol. 5318, pp. 790–803. Springer, Heidelberg (2008)
Bonino, D., Corno, F.: DogSim: A State Chart Simulator for Domotic Environments. In: 8th IEEE International Conference on Pervasive Computing and Communications Workshops (PERCOM Workshops), pp. 208–213 (2010), doi:10.1109/PERCOMW.2010.5470666
Booch, G., Rumbaugh, J., Jacobson, I.: Unified Modeling Language User Guide. The Addison Wesley, Reading (1998) ISBN 0-201-57168-4
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986)
De Nicola, R.: Three Logics for Branching Bisimulation. Journal of the Association for Computing Machinery 42(2), 458–487 (1995)
Ducatel, K., Bogdanowicz, M., Scapolo, F., Leijten, J., Burgelman, J.C.: Scenarios for Ambient Intelligence in 2010. Tech. rep., ISTAG: IST Advisory Group (2001)
Gnesi, S., Latella, D., Massink, M.: Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking. Journal of Logic and Algebraic Programming 51(1), 43–75 (2002)
Gnesi, S., Mazzanti, F.: On the fly model checking UML State Machines. In: ACIS International Conference on Software Engineering Research, Management and Applications, pp. 331–3382 (2004)
Gnesi, S., Mazzanti, F.: A Model Checking Verification Environments for UML Statecharts. In: Proceedings of the XLIII Congresso Annuale AICA (2005)
Mazzanti, F.: UMC 3.3 User Guide, ISTI Technical Report 2006-TR-33. ISTI-NNR Pisa-Italy (2006)
OSGi Service Platform release 4. Tech. rep., The OSGi alliance (2007)
State chart XML (SCXML): State Machine Notation for Control Abstraction. Tech. rep., W3C (2010), http://www.w3.org/TR/scxml/
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
Corno, F., Sanaullah, M. (2011). Design Time Methodology for the Formal Verification of Intelligent Domotic Environments. In: Novais, P., Preuveneers, D., Corchado, J.M. (eds) Ambient Intelligence - Software and Applications. Advances in Intelligent and Soft Computing, vol 92. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19937-0_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-19937-0_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19936-3
Online ISBN: 978-3-642-19937-0
eBook Packages: EngineeringEngineering (R0)