{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T14:10:28Z","timestamp":1761401428390},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,6,20]],"date-time":"2009-06-20T00:00:00Z","timestamp":1245456000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2009,9]]},"DOI":"10.1007\/s11334-009-0092-5","type":"journal-article","created":{"date-parts":[[2009,6,19]],"date-time":"2009-06-19T04:11:35Z","timestamp":1245384695000},"page":"181-196","source":"Crossref","is-referenced-by-count":2,"title":["Using formal methods to increase confidence in a home network system implementation: a case study"],"prefix":"10.1007","volume":"5","author":[{"given":"Lydie","family":"du Bousquet","sequence":"first","affiliation":[]},{"given":"Masahide","family":"Nakamura","sequence":"additional","affiliation":[]},{"given":"Ben","family":"Yan","sequence":"additional","affiliation":[]},{"given":"Hiroshi","family":"Igaki","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,6,20]]},"reference":[{"key":"92_CR1","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1007\/s10270-004-0058-x","volume":"4","author":"W Ahrendt","year":"2005","unstructured":"Ahrendt W, Baar T, Beckert B, Bubel R, Giese M, H\u00e4hnle R, Menzel W, Mostowski W, Roth A, Schlager S, Schmitt PH (2005) The KeY Tool. Softw Syst Model 4: 32\u201354","journal-title":"Softw Syst Model"},{"key":"92_CR2","doi-asserted-by":"crossref","unstructured":"Balfe S, Li S, Zhou J (2006) Pervasive trusted computing. In: 2nd international workshop on security, privacy and trust in pervasive and ubiquitous computing (SecPerU), pp 88\u201394. IEEE Computer Society, Lyon","DOI":"10.1109\/SECPERU.2006.14"},{"key":"92_CR3","doi-asserted-by":"crossref","unstructured":"Bartetzko D, Fischer C, M\u00f6ller M, Wehrheim H (2001) Jass-Java with Assertions. Electr Notes Theor Comput Sci 55(2)","DOI":"10.1016\/S1571-0661(04)00247-6"},{"key":"92_CR4","doi-asserted-by":"crossref","unstructured":"Beckert B, H\u00e4hnle R, Schmitt PH (eds) (2007) Verification of object-oriented software: the KeY approach. LNCS 4334. Springer","DOI":"10.1007\/978-3-540-69061-0"},{"key":"92_CR5","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/3-540-27139-2_2","volume-title":"Ambient intelligence","author":"J Bohn","year":"2005","unstructured":"Bohn J, Coroama V, Langheinrich M, Mattern F, Rohs M (2005) Social, economic, and ethical implications of ambient intelligence and ubiquitous computing. In: Weber W, Rabaey J, Aarts E (eds) Ambient intelligence. Springer, Berlin, pp 5\u201329"},{"key":"92_CR6","doi-asserted-by":"crossref","unstructured":"Bousquet L, Ledru Y, Maury O, Oriat C, Lanet JL (2004) A case study in JML-based software validation (short paper). In: Proceedings of 19th Int. IEEE Conf. on Automated Sofware Engineering (ASE\u201904), pp 294\u2013297","DOI":"10.1109\/ASE.2004.1342750"},{"issue":"3","key":"92_CR7","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L Burdy","year":"2005","unstructured":"Burdy L, Cheon Y, Cok DR, Ernst MD, Kiniry JR, Leavens GT, Leino KRM, Poll E (2005) An overview of JML tools and applications. STTT 7(3): 212\u2013232","journal-title":"STTT"},{"key":"92_CR8","doi-asserted-by":"crossref","unstructured":"Busi N, Gorrieri R, Guidi C, Lucchi R, Zavattaro G. (2005) Towards a formal framework for choreography. In: Enabling technologies: infrastructure for collaborative enterprise. 14th IEEE international workshops on 13\u201315 June 2005, pp 107\u2013112","DOI":"10.1109\/WETICE.2005.57"},{"key":"92_CR9","doi-asserted-by":"crossref","unstructured":"Candolin C (2007) A security framework for service oriented architectures. In: Military communications conference, 2007. MILCOM. IEEE, pp 1\u20136, 29\u201331 Oct 2007","DOI":"10.1109\/MILCOM.2007.4455332"},{"issue":"2","key":"92_CR10","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/MITP.2006.51","volume":"8","author":"G Canfora","year":"2006","unstructured":"Canfora G, Di Penta M (2006) Testing services and service-centric systems: challenges and opportunities. IT Prof 8(2): 10\u201317","journal-title":"IT Prof"},{"key":"92_CR11","doi-asserted-by":"crossref","unstructured":"Cheon Y, Leavens G (2002) A simple and practical approach to unit testing: the JML and JUnit way. In: ECOOP 2002. LNCS, vol 2474. Springer, pp 231\u2013255","DOI":"10.1007\/3-540-47993-7_10"},{"issue":"5","key":"92_CR12","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1109\/52.536462","volume":"13","author":"D Cohen","year":"1996","unstructured":"Cohen D, Dalal S, Parelius J, Patton G (1996) The combinatorial design approach to automatic test generation. IEEE Softw 13(5): 83\u201388","journal-title":"IEEE Softw"},{"key":"92_CR13","doi-asserted-by":"crossref","unstructured":"Controneo D, Di Flora C, Russo S (2003) Improving dependability of service oriented architectures for pervasive computing. Object-oriented real-time dependable systems, 2003. (WORDS 2003). In: Proceedings of the eighth international workshop on 15\u201317 Jan 2003, pp 74\u201381","DOI":"10.1109\/WORDS.2003.1218068"},{"key":"92_CR14","doi-asserted-by":"crossref","unstructured":"Dai G, Bai X, Wang F, Dai F (2007) Contract-based testing for web services. In: 31st annual international computer software and applications conference (COMPSAC). IEEE Computer Society, Beijing, China, pp 517\u2013526","DOI":"10.1109\/COMPSAC.2007.100"},{"key":"92_CR15","doi-asserted-by":"crossref","unstructured":"Dragoni N, Massacci F, Naliuka K, Siahaan I (2007) Security- by-contract: toward a semantics for digital signatures on mobile code. In: 4th European public key infrastructure workshop: theory and practice (EuroPKI). LNCS, vol 4582. Springer, Palma de Mallorca, Spain, pp 297\u2013312","DOI":"10.1007\/978-3-540-73408-6_21"},{"key":"92_CR16","doi-asserted-by":"crossref","unstructured":"du Bousquet L (1999) Feature interaction detection using testing and model-checking, experience report. In: World congress on formal methods. LNCS, vol 1708, Springer, Toulouse, pp 622\u2013641","DOI":"10.1007\/3-540-48119-2_35"},{"key":"92_CR17","doi-asserted-by":"crossref","unstructured":"Flanagan C, Leino KRM, Lillibridge M, Nelson G, Saxe JB, Stata R (2002) Extended static checking for Java. In: Proc. of the ACM SIGPLAN 2002 conference on programming language design and implementation. ACM Press, pp 234\u2013245","DOI":"10.1145\/512529.512558"},{"key":"92_CR18","doi-asserted-by":"crossref","unstructured":"Foster H, Uchitel S, Magee J, Kramer J (2003) Model-based verification of Web service compositions. In: Automated software engineering, 2003. Proceedings. 18th IEEE international conference on 6\u201310 Oct 2003, pp 152\u2013161","DOI":"10.1109\/ASE.2003.1240303"},{"issue":"1","key":"92_CR19","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1109\/MPRV.2006.10","volume":"5","author":"D Geer","year":"2006","unstructured":"Geer D (2006) Nanotechnology: the growing impact of shrinking computers. Pervasive Comput 5(1): 7\u201311","journal-title":"Pervasive Comput"},{"key":"92_CR20","doi-asserted-by":"crossref","unstructured":"Jackson M (1999) The role of formalism in method. In: Formal methods, world congress on formal methods in the development of computing systems (FM99). LNCS, vol 1708. Springer, Toulouse, p 56","DOI":"10.1007\/3-540-48119-2_5"},{"key":"92_CR21","unstructured":"The JML Home Page (2005). http:\/\/www.jmlspecs.org"},{"issue":"3","key":"92_CR22","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/s10703-005-3400-1","volume":"27","author":"M Karaorman","year":"2005","unstructured":"Karaorman M, Abercrombie P (2005) Contractor: introducing design-by-contract to java using reflective bytecode instrumentation. Form Methods Syst Des 27(3): 275\u2013312","journal-title":"Form Methods Syst Des"},{"key":"92_CR23","doi-asserted-by":"crossref","unstructured":"Karaorman M, Holzle U, Bruno J (1999) Contractor: a reflective java library to support design by contract. Tech. rep., Santa Barbara","DOI":"10.1007\/3-540-48443-4_18"},{"key":"92_CR24","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1109\/MCOM.2003.1244934","volume":"41","author":"M Kolberg","year":"2003","unstructured":"Kolberg M, Magill E, Wilson M (2003) Compatibility issues between services supporting networked appliances. IEEE Commun Mag 41: 136\u2013147","journal-title":"IEEE Commun Mag"},{"key":"92_CR25","doi-asserted-by":"crossref","unstructured":"Lamparter S, Luckner S, Mutschler S (2007) Formal specification of web service contracts for automated contracting and monitoring. In: 40th Hawaii international conference on systems science (HICSS). IEEE Computer Society, Big Island, p 63","DOI":"10.1109\/HICSS.2007.232"},{"issue":"1","key":"92_CR26","first-page":"132","volume":"15","author":"M Langheinrich","year":"2005","unstructured":"Langheinrich M, Coroama V, Bohn J, Mattern F (2005) Living in a smart environment\u2014implications for the coming ubiquitous information society. Telecommun Rev 15(1): 132\u2013143","journal-title":"Telecommun Rev"},{"key":"92_CR27","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral specifications of businesses and systems","author":"G Leavens","year":"1999","unstructured":"Leavens G, Baker A, Ruby C (1999) JML: a notation for detailed design. In: Kilov H, Rumpe B, Simmonds I (eds) Behavioral specifications of businesses and systems. Kluwer, Dordrecht, pp 175\u2013188"},{"key":"92_CR28","doi-asserted-by":"crossref","unstructured":"Ledru Y, du Bousquet L, Maury O, Bontron P (2004) Filtering TOBIAS combinatorial test suites. In: Fundamental approaches to software engineering (FASE\u201904). LNCS, vol (to appear). Springer, Barcelona","DOI":"10.1007\/978-3-540-24721-0_21"},{"key":"92_CR29","doi-asserted-by":"crossref","unstructured":"Loke SW (2003) Service-oriented device ecology workflows. In: First international conference on service-oriented computing (ICSOC 2003). LNCS, vol 2910. Springer, Trento, pp 559\u2013574","DOI":"10.1007\/978-3-540-24593-3_38"},{"key":"92_CR30","unstructured":"Matsushita Electric Industrial Co., L Kurashi Net (jp). http:\/\/national.jp\/appliance\/product\/kurashi-net\/"},{"key":"92_CR31","unstructured":"Meyer B Object-oriented software construction, 2nd edn"},{"issue":"10","key":"92_CR32","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer B (1992) design by contract. Computer 25(10): 40\u201351","journal-title":"Computer"},{"key":"92_CR33","unstructured":"Nakajima S (2002) Model-checking verification for reliable web services. In: Workshop on Object-Oriented Web Services, collocated with OOPSLA"},{"key":"92_CR34","doi-asserted-by":"crossref","unstructured":"Nakamura M, Tanaka A, Igaki H, Tamada H, Matsumoto K (2006) Adapting legacy home appliances to home network systems using web services. In: Int. Conf. on Web Services (ICWS 2006). IEEE, pp 849\u2013858","DOI":"10.1109\/ICWS.2006.23"},{"key":"92_CR35","doi-asserted-by":"crossref","unstructured":"Nakamura M, Tanaka A, Igaki H, Tamada H, Matsumoto K (2008) Constructing home network systems and integrated services using legacy home appliances and web services. Int J Web Serv Res, to appear","DOI":"10.4018\/jwsr.2008010105"},{"issue":"10","key":"92_CR36","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1145\/944217.944233","volume":"46","author":"MP Papazoglou","year":"2003","unstructured":"Papazoglou MP, Georgakopoulos D (2003) Special issue: service-oriented computing. Introduction. Commun ACM 46(10): 24\u201328","journal-title":"Commun ACM"},{"key":"92_CR37","unstructured":"Pfadenhauer K, Dustdar S, Kittl B (2005) Challenges and solutions for model-driven Web service composition. Enabling technologies: infrastructure for collaborative enterprise, 2005. In: 14th IEEE international workshops on 13\u201315 June 2005, pp 126\u2013131"},{"key":"92_CR38","unstructured":"Plath M, Ryan MD (2000) The feature construct for SMV: semantics. In: Feature interactions in telecommunications and software systems VI. Glasgow, pp 129\u2013144"},{"key":"92_CR39","doi-asserted-by":"crossref","unstructured":"Rushby JM (1999) Mechanized formal methods: where next? In: Formal methods, world congress on formal methods in the development of computing systems (FM99). LNCS, vol 1708. Springer, Toulouse, pp 48\u201351","DOI":"10.1007\/3-540-48119-2_3"},{"key":"92_CR40","unstructured":"TOSHIBA: Toshiba home network: feminity. http:\/\/www3.toshiba.co.jp\/feminity\/feminity_eng\/"},{"issue":"7","key":"92_CR41","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1145\/159544.159617","volume":"36","author":"M Weiser","year":"1993","unstructured":"Weiser M (1993) Some computer science issues in ubiquitous computing. Commun ACM 36(7): 74\u201384","journal-title":"Commun ACM"},{"key":"92_CR42","doi-asserted-by":"crossref","unstructured":"Yan B, Nakamura M, du Bousquet L, ichi Matsumoto K (2007) Characterizing safety of integrated services in home network system. In: 5th international conference on smart homes and health telematics (ICOST), LNCS, vol. 4541. Springer, Nara, pp 130\u2013140","DOI":"10.1007\/978-3-540-73035-4_14"},{"key":"92_CR43","unstructured":"Yi X, Kochut K (2004) A CP-nets-based design and verification framework for Web services composition. IEEE int. conf. on web services, 6\u20139 July 2004, pp 756\u2013760"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-009-0092-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-009-0092-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-009-0092-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T09:47:44Z","timestamp":1559382464000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-009-0092-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,6,20]]},"references-count":43,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,9]]}},"alternative-id":["92"],"URL":"https:\/\/doi.org\/10.1007\/s11334-009-0092-5","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,6,20]]}}}