This Article 
 Bibliographic References 
 Add to: 
Tools for the Rapid Prototyping of Provably Correct Ambient Intelligence Applications
July-Aug. 2012 (vol. 38 no. 4)
pp. 975-991
A. Coronato, Inst. of High Performance Comput. & Networking (ICAR), Naples, Italy
G. De Pietro, Inst. of High Performance Comput. & Networking (ICAR), Naples, Italy
Ambient Intelligence technologies have not yet been widely adopted in safety critical scenarios. This principally has been due to fact that acceptable degrees of dependability have not been reached for the applications that rely on such technologies. However, the new critical application domains, like Ambient Assisted Living and Smart Hospitals, which are currently emerging, are increasing the need for methodologies and tools that can improve the reliability of the final systems. This paper presents a middleware architecture for safety critical Ambient Intelligence applications which provides the developer with services for runtime verification. It is now possible to continuously monitor and check the running system against correctness properties defined at design time. Moreover, a visual tool which allows the formal design of several of the characteristics of an Ambient Intelligence application and the automatic generation of setting up parameters and code for the middleware infrastructure is also presented.

[1] D.J. Cook, J.C. Augusto, and V.R. Jakkula, "Ambient Intelligence: Technologies, Applications, and Opportunities," Pervasive and Mobile Computing, vol. 5, no. 4, pp. 277-298, B7MF1-4W2W5PH-1/27ac602bb16ca409e2f70c13aa24ae0d5 , 2009.
[2] R.-G. Lee, K.-C. Chen, C.-C. Hsiao, and C.-L. Tseng, "A Mobile Care System with Alert Mechanism," IEEE Trans. Information Technology in Biomedicine, vol. 11, no. 5, pp. 507-517, Sept. 2007.
[3] A.E.K. Sobel and M.R. Clarkson, "Formal Methods Application: An Empirical Tale of Software Development," IEEE Trans. Software Eng., vol. 28, no. 3, pp. 308-320,, Mar. 2002.
[4] J.P. Bowen and V. Stavridou, Formal Methods and Software Safety, pp. 93-98. Pergamon Press, 1992.
[5] G.K. Saha, "Software Fault Avoidance Issues," Ubiquity, vol. 2006, pp. 5:1-5:15, , Nov. 2006.
[6] F.C. Gärtner, "Fundamentals of Fault-Tolerant Distributed Computing in Asynchronous Environments," ACM Computing Surveys, vol. 31, pp. 1-26,, Mar. 1999.
[7] D. Karlsson, P. Eles, and Z. Peng, "Formal Verification of Component-Based Designs," Design Automation for Embedded Systems, vol. 11, pp. 49-90, , 2007.
[8] R.M. Hierons, K. Bogdanov, J.P. Bowen, R. Cleaveland, J. Derrick, J. Dick, M. Gheorghe, M. Harman, K. Kapoor, P. Krause, G. Lüttgen, A.J.H. Simons, S. Vilkomir, M.R. Woodward, and H. Zedan, "Using Formal Specifications to Support Testing," ACM Computing Surveys, vol. 41, pp. 9:1-9:76, , Feb. 2009.
[9] E.M. ClarkJr., O. Grumberg, and D.A. Peled, Model Checking. The MIT Press, 1999.
[10] L.C. Paulson, "The Foundation of a Generic Theorem Prover," J. Automated Reasoning, vol. 5, pp. 363-397, http://portal.acm.orgcitation.cfm?id=67173.67178 , Sept. 1989.
[11] W. Charatonik and J.-M. Talbot, "The Decidability of Model Checking Mobile Ambients," Proc. 15th Int'l Workshop Computer Science Logic), pp. 339-354, http://portal.acm.orgcitation. cfm?id=647851.737396 , 2001.
[12] G. Roşu and K. Havelund, "Rewriting-Based Techniques for Runtime Verification," Automated Software Eng., vol. 12, pp. 151-197, http://portal.acm.orgcitation.cfm?id=1058042.1058048 , Apr. 2005.
[13] A. Hall, "Seven Myths of Formal Methods," IEEE Software, vol. 7, no. 5, pp. 11-19,, Sept. 1990.
[14] L. Cardelli and A.D. Gordon, "Mobile Ambients," Theoretical Computer Science, vol. 240, pp. 177-213, http://portal.acm.orgcitation.cfm?id=340593.340606 , June 2000.
[15] A. Ranganathan and R.H. Campbell, "Provably Correct Pervasive Computing Environments," Proc. IEEE Sixth Ann. Int'l Conf. Pervasive Computing and Comm., pp. 160-169, http://portal. acm.orgcitation.cfm?id=1371610.1372949 , 2008.
[16] T. Weis, C. Becker, and E. Brändle, "Towards a Programming Paradigm for Pervasive Applications Based on the Ambient Calculus," Proc. Int'l Workshop Combining Theory and Systems Building in Pervasive Computing, 2006.
[17] G. Schiele, M. Handte, and C. Becker, "Good Manners for Pervasive Computing—An Approach Based on the Ambient Calculus," Proc. IEEE Fifth Ann. Int'l Conf. Pervasive Computing and Comm. Workshops, pp. 585-588, , 2007.
[18] L. Cardelli and A.D. Gordon, "Anytime Anywhere: Modal Logics for Mobile Ambients," Proc. 27th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp. 365-377, http://doi.acm. org/10.1145325694.325742 , 2000.
[19] W. Charatonik, S.D. Zilio, A.D. Gordon, S. Mukhopadhyay, and J.-M. Talbot, "Model Checking Mobile Ambients," Theoretical Computer Science, vol. 308, nos. 1-3, pp. 277-331, B6V1G-47C49JM-1/2518046be248a9992c4f1b9f060357768 , 2003.
[20] R. Mardare, C. Priami, P. Quaglia, and O. Vagin, "Model Checking Biological Systems Described Using Ambient Calculus," Proc. Int'l Conf. Computational Methods in Systems Biology, V. Danos and V. Schachter, eds., pp. 85-103, , 2005.
[21] A. Cimatti, E.M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella, "Nusmv 2: An Opensource Tool for Symbolic Model Checking," Proc. 14th Int'l Conf. Computer Aided Verification, pp. 359-364, http://portal. acm.orgcitation.cfm?id=647771.734431 , 2002.
[22] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications," ACM Trans. Programming Languages and Systems, vol. 8, pp. 244-263,, Apr. 1986.
[23] C. Kern and M.R. Greenstreet, "Formal Verification in Hardware Design: A Survey," ACM Trans. Design Automation of Electronic Systems, vol. 4, pp. 123-193,, Apr. 1999.
[24] O. Kupferman, M.Y. Vardi, and P. Wolper, "An Automata-Theoretic Approach to Branching-Time Model Checking," J. ACM, vol. 47, pp. 312-360,, Mar. 2000.
[25] F. Wang, "Formal Verification of Timed Systems: A Survey and Perspective," Proc. IEEE, vol. 92, no. 8, pp. 1281-1282, Aug. 2004.
[26] G.J. Holzmann, "The Model Checker Spin," IEEE Trans. Software Eng., vol. 23, no. 5, pp. 279-295, http://portal.acm.orgcitation.cfm?id=260897.260902 , May 1997.
[27] K.L. McMillan, Symbolic Model Checking. Kluwer Academic Publishers, 1993.
[28] Z. Chen and S. Fickas, "Do No Harm: Model Checking ehome Applications," Proc. First Int'l Workshop Software Eng. for Pervasive Computing Applications, Systems, and Environments, p. 8,, 2007.
[29] R. Hall and H. Cervantes, "An OSGI Implementation and Experience Report," Proc. IEEE First Consumer Comm. and Networking Conf., pp. 394-399, 2004.
[30] M. Leucker and C. Schallhart, "A Brief Account of Runtime Verification," J. Logic and Algebraic Programming, vol. 78, no. 5, pp. 293-303, 2009.
[31] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J.F. Quesada, "Maude: Specification and Programming in Rewriting Logic," Theoretical Computer Science, vol. 285, pp. 187-243, http://portal.acm.orgcitation.cfm?id=633559. 633563 , Aug. 2002.
[32] M.-R. Tazari, F. Furfari, J.-P.L. Ramos, and E. Ferro, "The Persona Service Platform for AAL Spaces," Handbook of Ambient Intelligence and Smart Environments, H. Nakashima, H. Aghajan, and J.C. Augusto, eds., pp. 1171-1199, Springer, , 2010.
[33] M. Lipprandt, M. Eichelberg, W. Thronicke, J. Krüger, I. Drüke, D. Willemsen, C. Busch, C. Fiehe, E. Zeeb, and A. Hein, "Osami-d: An Open Service Platform for Healthcare Monitoring Applications," Proc. Second Conf. Human System Interactions), pp. 136-142, http://portal.acm.orgcitation.cfm?id=1689359.1689385 , 2009.
[34] G. Fortino, A. Guerrieri, F. Bellifemine, and R. Giannantonio, "Spine2: Developing bsn Applications on Heterogeneous Sensor Nodes," Proc. IEEE Int'l Symp. Industrial Embedded Systems, pp. 128-131, 2009.
[35] P. Felber and P. Narasimhan, "Experiences, Strategies, and Challenges in Building Fault-Tolerant Corba Systems," IEEE Trans. Computers, vol. 53, no. 5, pp. 497-511, http://portal. acm.orgcitation.cfm?id=977244.977334 , May 2004.
[36] L. Zeng, B. Benatallah, A.H.H. Ngu, M. Dumas, J. Kalagnanam, and H. Chang, "QoS-Aware Middleware for Web Services Composition," IEEE Trans. Software Eng., vol. 30, no. 5, pp. 311-327, May 2004.
[37] A. Corsaro and D.C. Schmidt, "The Design and Performance of Real-Time Java Middleware," IEEE Trans. Parallel and Distributed Systems, vol. 14, no. 11, pp. 1155-1167, Nov. 2003.
[38] A. Coronato and G. De Pietro, "Formal Specification of Wireless and Pervasive Healthcare Applications," ACM Trans. Embedded Computing Systems, vol. 10, pp. 1-18, , Aug. 2010.
[39] A. Coronato and G. De Pietro, "Formal Specification and Verification of Ubiquitous and Pervasive Systems," ACM Autonomous and Adaptive Systems, vol. 6, pp. 9:1-9:6, http://doi. acm.org1921641.1921650, Feb. 2011.
[40] A. Coronato and G.D. Pietro, "Formal Design of Ambient Intelligence Applications," Computer, vol. 43, no. 12, pp. 60-68, Dec. 2010.
[41] G. Acampora and V. Loia, "Fuzzy Control Interoperability and Scalability for Adaptive Domotic Framework," IEEE Trans. Industrial Informatics, vol. 1, no. 2, pp. 97-111, May 2005.
[42] G. Acampora, M. Gaeta, V. Loia, and A.V. Vasilakos, "Interoperable and Adaptive Fuzzy Services for Ambient Intelligence Applications," ACM Trans. Autonomous and Adaptive Systems, vol. 5, pp. 8:1-8:26, , May 2010.
[43] G. Păun, "Computing with Membranes," J. Computer and System Sciences vol. 61, pp. 108-143, http://portal.acm.orgcitation. cfm?id=353298.353304 , Aug. 2000.
[44] G. Acampora and V. Loia, "A Proposal of Multi-Agent Simulation System for Membrane Computing Devices," Proc. IEEE Congress Evolutionary Computation, pp. 4100-4107, 2007.
[45] P.T. Eugster, P.A. Felber, R. Guerraoui, and A.-M. Kermarrec, "The Many Faces of Publish/Subscribe," ACM Computing Surveys, vol. 35, pp. 114-131,, June 2003.
[46] A. Coronato, M. Esposito, and G. De Pietro, "A Multimodal Semantic Location Service for Intelligent Environments: An Application for Smart Hospitals," Personal Ubiquitous Computing vol. 13, pp. 527-538, , Oct. 2009.
[47] J. Wu, L. Huang, D. Wang, and F. Shen, "R-OSGI-Based Architecture of Distributed Smart Home System," IEEE Trans. Consumer Electronics, vol. 54, no. 3, pp. 1166-1172, Aug. 2008.
[48] C. Hoare, J. Misra, G.T. Leavens, and N. Shankar, "The Verified Software Initiative: A Manifesto," ACM Computing Surveys, vol. 41, pp. 22:1-22:8, , Oct. 2009.

Index Terms:
ubiquitous computing,middleware,safety-critical software,software prototyping,pervasive computing,rapid prototyping,ambient intelligence applications,safety critical scenarios,new critical application domains,ambient assisted living,smart hospitals,middleware architecture,runtime verification,visual tool,formal design,automatic generation,Calculus,Runtime,Middleware,Ambient intelligence,Monitoring,Biomembranes,Mobile communication,designing tools,Safety critical ambient intelligence systems,middleware infrastructures
A. Coronato, G. De Pietro, "Tools for the Rapid Prototyping of Provably Correct Ambient Intelligence Applications," IEEE Transactions on Software Engineering, vol. 38, no. 4, pp. 975-991, July-Aug. 2012, doi:10.1109/TSE.2011.67
Usage of this product signifies your acceptance of the Terms of Use.