Sage Journals: Discover world-class research

Abstract

Modern Smart Environments (SmE) are equipped with a multitude of devices and sensors aimed at intelligent services. The variety of devices has raised a major problem of managing SmE. An increasingly adopted solution to the problem is the modeling of goals and intentions, and then using artificial intelligence to control the respective SmE accordingly. Generally, the solution advocates that the goals can be achieved by controlling the evolution of the states of the devices. In order to automatically reach a particular state, a sophisticated solution is required through which the respective commands, notifications and their correct sequence can be discovered and enforced on the real devices.

In this paper, a comprehensive methodology is proposed by considering a) the composite nature of the state of an individual device; b) the possible variation of specific commands, notifications and their sequence based on the current states of the devices.

The methodology works at two levels: design-time and runtime. At design-time, it constructs the extended data and control flow behavioral graphs of the devices by using the concepts of a model checking approach. Then, at runtime, it uses these graphs for finding the reliable evolution through which the desired goal can be fulfilled. The proposed methodology is implemented over the Domotic Effects framework and a home automation system, i.e. Domotic OSGi Gateway (Dog). The implementation and experimentation details indicate the effectiveness of the proposed approach.

Keywords

Intelligent device activation high-level goals device interface and behavioral modeling statecharts model checking Domotic Effects

Get full access to this article

View all access options for this article.

References

[1]OSGi Alliance, Osgi service platform, core specification, release 4, version 4.1, OSGi Specification, 2007.

[2]

Amigoni,

Gatti,

Pinciroli and

Roveri, What planner for ambient intelligence applications? IEEE Transactions on Systems, Man and Cybernetics, Part A: Systems and Humans 35(1) (2005), 7–21, IEEE.

[3]

Baier and

Katoen, Principles of Model-Checking, The MIT Press, May 2008, ISBN-10: 0-262-02649-X, ISBN-13: 978-0-262-02649-9.

[4]

Barnett,

Akolkar,

Auburn et al., State chart xml (scxml): State machine notation for control abstraction, W3C Working Draft, 2007.

[5]

Bogdanov and

Holcombe, Statechart testing method for aircraft control systems, Software Testing, Verification and Reliability 11(1) (2001), 39–54.

[6]

Bonhomme,

Campo,

Esteve and

Guennec, Methodology and tools for the design and verification of a smart management system for home comfort, in: 4th International IEEE Conference on Intelligent Systems, IEEE, 2008, pp. 242–24-7.

[7]

Bonino,

Castellina and

Corno, The DOG gateway: Enabling ontology-based intelligent domotic environments, IEEE Transactions on Consumer Electronics 54(4) (November 2008), 1656–1664, IEEE.

[8]

Bonino and

Corno, DogOnt – ontology modeling for intelligent domotic environments, in: International Semantic Web Conference,

Sheth,

Staab,

Dean,

Paolucci,

Maynard,

Finin and

Thirunarayan, eds, LNCS, Vol. 5318, Springer-Verlag, October 2008, pp. 790–803.

[9]

Bonino and

Corno, DogSim: A state chart simulator for Domotic Environments, in: 8th IEEE International Conference on Pervasive Computing and Communications (PERCOM Workshops), IEEE, 2010, pp. 208–213.

10.

[10]

Chen,

Finin and

Joshi, A context broker for building smart meeting rooms, in: Proc. of the Knowledge Representation and Ontology for Autonomous Systems Symposium, Defense Technical Information Center, 2004.

11.

[11]

Chen,

Perich,

Finin and

Joshi, Soupa: Standard ontology for ubiquitous and pervasive applications, in: The First Annual International Conference on Mobile and Ubiquitous Systems: Networking and Services, IEEE Computer Society, August 2004, pp. 258–267.

12.

[12]

Cheng,

Wang and

Chen, An adaptive scenario based reasoning system cross smart houses, in: 9th International Symposium on Communications and Information Technology, IEEE, 2009, pp. 549–554.

13.

[13]

E.M.

Clarke,

E.A.

Emerson and

A.P.

Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems 8(2) (April 1986), 244–263, ACM.

14.

[14]

Coen, Design principles for intelligent environments, in: Proc. of the Fifteenth National/tenth Conference on Artificial Intelligence/Innovative Applications of Artificial Intelligence, American Association for Artificial Intelligence, Menlo Park, CA, USA, 1998, pp. 547–554.

15.

[15]

Cook, Multi-agent smart environments, Journal of Ambient Intelligence and Smart Environments 1(1) (2009), 51–55, IOS Press.

16.

[16]

Cook, The complexity of theorem-proving procedures, in: Proc. of the Third Annual ACM Symposium on Theory of Computing, ACM, 1971, pp. 151–158.

17.

[17]

Corno and

Razzak, Intelligent energy optimization for user intelligible goals in smart home environments, IEEE Transactions on Smart Grid 3(4) (2012), 2128–2135, IEEE.

18.

[18]

Corno and

Razzak, Sat based enforcement of domotic effects in smart environments, Journal of Ambient Intelligence and Humanized Computing 5(4) (2013), 565–579, Springer-Berlin-Heidelberg.

19.

[19]

Corno and

Sanaullah, Formal verification of device state chart models, in: 7th International Conference on Intelligent Environments, IEEE, July 2011, pp. 66–73.

20.

[20]

Cousot and

Cousot, Abstract interpretation frameworks, Journal of Logic and Computation 2(4) (1992), 511–547, Oxford University Press.

21.

[21]

Davidoff,

Lee,

Yiu,

Zimmerman and

Dey, Principles of smart home control, in: Proc. of the 8th International Conference on Ubiquitous Computing, Springer-Verlag, 2006, pp. 19–34.

22.

[22]

Dibowski,

Ploennigs and

Kabitzsch, Automated design of building automation systems, IEEE Transactions on Industrial Electronics 57(11) (2010), 3606–3613, IEEE.

23.

[23]

Dijkstra, A note on two problems in connexion with graphs, Numerische Mathematik 1(1) (1959), 269–271, Springer.

24.

[24]

Encarnaçao and

Kirste, Ambient intelligence: Towards smart appliance ensembles, in: From Integrated Publication and Information Systems to Information and Knowledge Environments, Springer, 2005, pp. 261–270.

25.

[25]

Erol,

Hendler and

Nau, Complexity results for HTN planning, Annals of Mathematics and Artificial Intelligence 18(1) (1996), 69–93, Springer.

26.

[26]

Fensel, Ontologies: A Silver Bullet for Knowledge Management and Electronic Commerce, Springer-Verlag, New York, NY, USA, 2001.

27.

[27]

Fredman and

Tarjan, Fibonacci heaps and their uses in improved network optimization algorithms, Journal of the ACM 34(3) (1987), 596–615.

28.

[28]

Gilks,

Richardson and

Spiegelhalter, Markov Chain Monte Carlo in Practice, 2, Chapman & Hall – CRC Press, 1996.

29.

[29]

Gnesi and

Mazzanti, A model checking verification environments for uml statecharts, in: Proc. of the XLIII Congresso Annuale AICA, Udine, 2005.

30.

[30]

Gouin-Vallerand,

Abdulrazak,

Giroux and

A.K.

Dey, A context-aware service provision system for smart environments based on the user interaction modalities, Journal of Ambient Intelligence and Smart Environments 5(1) (2013), 47–64, IOS Press.

31.

[31]

Gruber

et al., A translation approach to portable ontology specifications, Knowledge Acquisition 5(2) (1993), 199–220, Elsevier.

32.

[32]

Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming 8(3) (1987), 231–274, Elsevier.

33.

[33]

Heider and

Kirste, Supporting goal-based interaction with dynamic intelligent environments, in: The 15th European Conference on Artificial Intelligence, IOS Press, 2002, pp. 596–602, Fraunhofer Publica, Germany.

34.

[34]

Hellenschmidt, Distributed implementation of a self-organizing decentralized multimedia appliance middleware, in: Mobile Computing and Ambient Intelligence: The Challenge of Multimedia,

Davies,

Kirste and

Schumann, eds, Dagstuhl Seminar Proceedings, Vol. 05181, Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany, 2005.

35.

[35]

Hong,

Kim,

Cha,

Bae and

Ural, A test sequence selection method for statecharts, Software Testing, Verification & Reliability 10(4) (2000), 203–227, John Wiley & Sons.

36.

[36]

Hong,

Lee and

Sokolsky, Automatic test generation from statecharts using model checking, in: Proc. of FATES’01, Workshop on Formal Approaches to Testing of Software, Aalborg, Denmark, BRICS Notes Series, Vols NS-01-4(4), 2001, pp. 15–30.

37.

[37]

IsbellJr.,

Omojokun and

Pierce, From devices to tasks: Automatic task prediction for personalized appliance control, Personal and Ubiquitous Computing 8(3–4) (July 2004), 146–153, Springer-Verlag.

38.

[38]

M.R.

Kakoee,

Shojaei,

Ghasemzadeh,

Sirjani and

Navabi, A new approach for design and verification of transaction level models, in: IEEE International Symposium on Circuits and Systems, May 2007, pp. 3760–3763.

39.

[39]

Kaldeli,

Warriach,

Bresser,

Lazovik and

Aiello, Interoperation, composition and simulation of services at home, in: Service-Oriented Computing, Springer, 2010, pp. 167–181.

40.

[40]

Kansomkeat and

Rivepiboon, Automated-generating test case using uml statechart diagrams, in: Proc. of the 2003 Annual Research Conference of the South African Institute of Computer Scientists and Information Technologists on Enablement Through Technology, South African Institute for Computer Scientists and Information Technologists, 2003, pp. 296–300.

41.

[41]

Katasonov, Enabling non-programmers to develop smart environment applications, in: IEEE Symposium on Computers and Communications, IEEE, 2010, pp. 1059–1064.

42.

[42]

Kramer,

Noronha and

Vergo, A user-centered design approach to personalization, Communications of the ACM 43(8) (2000), 44–48.

43.

[43]

Le Berre and

Parrain, The Sat4j library, release 2.2 system description, Journal on Satisfiability, Boolean Modeling and Computation 7 (2010), 59–64, IOS Press.

44.

[44]

Leelaprute,

Nakamura,

Tsuchiya,

Matsumoto and

Kikuno, Describing and verifying integrated services of home network systems, in: 12th Asia-Pacific Software Engineering Conference, December 2005.

45.

[45]

Mazzanti, Designing UML models with UMC, Technical report, Technical Report 2009-TR-43, ISTI-CNR-Pisa, Italy, 2009.

46.

[46]

McGuinness,

Harmelen et al., Owl web ontology language overview, W3C Recommendation 10(3) (2004), W3C.

47.

[47]

Meshkova,

Riihijarvi,

Mahonen and

Kavadias, Modeling the home environment using ontology with applications in software configuration management, in: International Conference on Telecommunications, IEEE, 2008, pp. 1–6.

48.

[48]

Muthiayen, Animation and formal verification of real-time reactive systems in an object-oriented environment, Thesis, Department of Computer Science, Concordia University, 1996.

49.

[49]

Nakamura,

Tanaka,

Igaki,

Tamada and

K.-i.

Matsumoto, Constructing home network systems and integrated services using legacy home appliances and web services, International Journal of Web Services Research 5(1) (2008), 82–98, IGI Global.

50.

[50]

I.H.

Networking, Service gateway architecture for a smart home, IEEE Communications Magazine (2002), 126–132, IEEE.

51.

[51]

Niezen,

B.J.

van der Vlist,

Hu and

L.M.

Feijs, From events to goals: Supporting semantic interaction in smart environments, in: IEEE Symposium on Computers and Communications, IEEE, 2010, pp. 1029–1034.

52.

[52]

Omojokun,

Isbell and

Dewan, Towards automatic personalization of device controls, IEEE Transactions on Consumer Electronics 55(1) (2009), 269–276, IEEE.

53.

[53]

Omojokun,

Pierce,

Isbell and

Dewan, Comparing end-user and intelligent remote control interface generation, Personal and Ubiquitous Computing 10(2–3) (2006), 136–143, Springer-Verlag.

54.

[54]

Pap,

Majzik and

Pataricza, Checking general safety criteria on UML statecharts, in: Computer Safety, Reliability and Security, Springer, 2001, pp. 46–55.

55.

[55]

Rashidi and

Cook, Keeping the resident in the loop: Adapting the smart home to the user, IEEE Transactions on Systems, Man and Cybernetics, Part A: Systems and Humans 39(5) (2009), 949–959, IEEE.

56.

[56]

Rouillard,

Le Pallec,

Tarby and

Marvie, Facilitating the design of multi-channel interfaces for ambient computing, in: Third International Conference on Advances in Computer-Human Interactions, IEEE, 2010, pp. 95–100.

57.

[57]

Rouillard and

Tarby, How to communicate smartly with your house? International Journal of Ad Hoc and Ubiquitous Computing 7(3) (2011), 155–162.

58.

[58]

Ryzhyk,

Chubb,

Kuz,

Le Sueur and

Heiser, Automatic device driver synthesis with Termite, in: Proc. of the 22nd ACM Symposium on Operating Systems Principles, ACM, 2009, pp. 73–86.

59.

[59]

Santiago,

Vijaykumar,

Guimarães,

Amaral and

Ferreira, An environment for automated test case generation from statechart-based and finite state machine-based behavioral models, in: IEEE International Conference on Software Testing Verification and Validation Workshop, IEEE, 2008, pp. 63–72.

60.

[60]

Sommaruga,

Perri and

Furfari, DomoML-env: An ontology for human home interaction, in: Proc. of the 2nd Italian Semantic Web Workshop, Trento, Italy, 14–16 December, 2005, pp. 14–16.

61.

[61]

Stone,

Carter,

Justice,

Keller and

Tung, Improved modeling and validation of command sequences using a checkable sequence language, in: IEEE Aerospace Conference, IEEE, March 2012, pp. 1–11.

62.

[62]

Wei, Abstraction for verification and refutation in model checking, PhD thesis, University of Toronto, 2009.

63.

[63]

Weiser, The computer for the 21st century, Scientific American 265(3) (September 1991), 94–104.