International Journal of Information Technology and Computer Science (IJITCS)
IJITCS Vol. 6, No. 10, 8 Sep. 2014
Cover page and Table of Contents: PDF (size: 510KB)
Verification of Generic Ubiquitous Middleware for Smart Home Using Coloured Petri Nets
Full Text (PDF, 510KB), PP.63-69
Views: 0 Downloads: 0
Author(s)
Madhusudanan. J
1,*
Anand. P
2
Hariharan. S
2
V. Prasanna Venkatesan
1
Index Terms
Smart Home, Coloured Petri Nets, Context
Abstract
Smart home is a relatively new technology, where we applied pervasive computing in all the aspects, so as to make our jobs or things that we normally do in-side the home in a very easier way. Originally, a smart home technology was used to control environmental systems such as lighting and heating; but recently the use of smart technology has been developed so that almost any electrical component within the home can be included in the system. Usually in pervasive computing, a middleware is developed to provide interaction between the user and device. In previous, a middleware is only suitable for specific Smart Home architecture, that can’t be applicable to any other architecture but the Generic Ubiquitous Middleware is suitable for different Smart Home architecture. This paper proposes that any smart home can be built with single architecture and it is verified using a Coloured Petri Nets tool. We have given a verification model of various Smart home Environments.
Cite This Paper
Madhusudanan. J, Anand. P, Hariharan. S, V. Prasanna Venkatesan, "Verification of Generic Ubiquitous Middleware for Smart Home Using Coloured Petri Nets", International Journal of Information Technology and Computer Science(IJITCS), vol.6, no.10, pp.63-69, 2014. DOI:10.5815/ijitcs.2014.10.09
Reference
[1]M. Satyanarayanan, “Pervasive Computing: Vision and Challenges”, To appear in IEEE Personal Communications, 2001.
[2]Kristian Ellebæk Kjær, “A Survey Of Context-Aware Middleware”, IEEE, 2010.
[3]K. Jensen, L.M. Kristensen, “Formal Definition of Non-hierarchical Coloured Petri Nets”, springer 2009.
[4]Karima Mahdi, Raida Elmansouri, Allaoua Chaoui, “On Transforming Business Patterns to Labeled Petri Nets Using Graph Grammars”, IJITCS 2013.
[5]Kurt Jensen, Lars Michael Kristensen, LisaWells “Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems”, springer 2007.
[6]A. Cimatti, E. Clarke, F. Giunchiglia, M. Roveri. NuSMV: A New Symbolic Model Verifier. In Proceedings of International Conference on Computer-Aided Verification (CAV’99). Pp. 495–499. 1999.
[7]G. J. Holzmann. The Spin Model Checker. Addison-Wesley, 2003.
[8]T. V. Group. VIS: A System for Verification and Synthesis. In Proceedings of the 8th International Conference on Computer Aided Verification. Pp. 428–432. 1996.
[9]U. Hustadt, B. Konev. TRP++ 2.0: A Temporal Resolution Prover. In Proceedings of Conference on Automated Deduction (CADE-19). Pp. 274–278. 2003.
[10]K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishing, 1993.
[11]J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, W. Yi. UPPAAL — a Tool Suite for Automatic Verification of Real–Time Systems. In Proceedings of Workshop on Verification and Control of Hybrid Systems III. Lecture Notes in Computer Science 1066, pp. 232–243. Springer Verlag, 1995.
[12]M. Bozga, C. Daws, O. Maler, A. Olivero, StavrosTripakis, S. Yovine. Kronos: A Model-Checking Tool for Real-Time Systems. In CAV ’98: Proceedings of the 10th International Conference on Computer Aided Verification. Pp. 546–550. Springer Verlag, 1998.
[13]A. Hinton, M. Kwiatkowska, G. Norman, D. Parker. PRISM: A Tool for Automatic Verification of Probabilistic Systems. In Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’06). Lecture Notes in Computer Science 3920, pp. 441–444. Springer, 2006.
[14]T. H´erault, R. Lassaigne, F. Magniette, S. Peyronnet. Approximate Probabilistic Model Checking. In Proc. 5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’04). Lecture Notes in Computer Science 2937, pp. 307–329. Springer, 2004.
[15]A. Kalaiselvi, V. Indhumathy, J. Madhusudanan, V. Prasanna Venkatesan, “Implementation of Generic Context Middleware for Context-Aware Applications”, International Journal of Engineering Research & Technology (IJERT), 2012.
[16]Jerome Hugues, Thomas Vergnaud, Laurent Pautet, “On the Formal Verification of Middleware Behavioral Properties”, ELSEVIER, 2005.
[17]Azza K. Nabih, Mostafa M. Gomaa, Hossam S. Osman, Gamal M. Aly, “Modeling, Simulation, and Control of Smart Homes Using Petri Nets”, International Journal of Smart Home, 2011.
[18]V. Indhumathy, A. Kalaiselvi, J. Madhusudanan, V. Prasanna Venkatesan, “A Generic Simulation Tool for Pervasive Devices Application”, International Journal of Engineering Research & Technology (IJERT), 2012.