{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:25:02Z","timestamp":1750307102442,"version":"3.41.0"},"reference-count":7,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2012,11,27]],"date-time":"2012-11-27T00:00:00Z","timestamp":1353974400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2012,11,27]]},"abstract":"<jats:p>Hybrid systems are characterized by combining discrete and continuous behaviors. Verification of hybrid systems is, in general, a diffcult task due to the potential complexity of the continuous dynamics. Currently, there are different formalisms and tools which are able to analyze specific types of hybrid systems, model checking being one of the most used approaches. In this paper, we describe an extension of Java PathFinder in order to analyze hybrid systems. We apply a general methodology which has been successfully used to extend Spin. This methodology is non-intrusive, and uses external libraries, such as the Parma Polyhedra Library, to abstract the continuous behavior of the hybrid system.<\/jats:p>","DOI":"10.1145\/2382756.2382793","type":"journal-article","created":{"date-parts":[[2012,11,29]],"date-time":"2012-11-29T15:02:27Z","timestamp":1354201347000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["An extension of Java PathFinder for hybrid systems"],"prefix":"10.1145","volume":"37","author":[{"given":"Laura","family":"Panizo","sequence":"first","affiliation":[{"name":"University of M\u00e1laga, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mar\u00eda","family":"del Mar Gallardo","sequence":"additional","affiliation":[{"name":"University of M\u00e1laga, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,11,27]]},"reference":[{"unstructured":"Nasa Ames Research Center Java PathFinder. http:\/\/babelsh.arc.nasa.gov\/trac\/jpf\/wiki\/WikiStart. Accessed: 24\/07\/2012.  Nasa Ames Research Center Java PathFinder. http:\/\/babelsh.arc.nasa.gov\/trac\/jpf\/wiki\/WikiStart. Accessed: 24\/07\/2012.","key":"e_1_2_1_1_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_2_1_3_1","first-page":"888","article-title":"Automotive engine control and hybrid systems: Challenges and opportunities","volume":"7","author":"Balluchi A.","year":"2000","unstructured":"Balluchi , A. , Benvenuti , L. , Benedetto , M. D. , Pinello , C. , and Sangiovanni-Vincentelli , A . Automotive engine control and hybrid systems: Challenges and opportunities . Procs. of the IEEE. Special Issue on Hybrid Systems 7 ( 2000 ), 888 -- 912 . Balluchi, A., Benvenuti, L., Benedetto, M. D., Pinello, C., and Sangiovanni-Vincentelli, A. Automotive engine control and hybrid systems: Challenges and opportunities. Procs. of the IEEE. Special Issue on Hybrid Systems 7 (2000), 888--912.","journal-title":"Procs. of the IEEE. Special Issue on Hybrid Systems"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.5555\/519167.828753"},{"key":"e_1_2_1_5_1","volume-title":"Procs. of PROLE 2010 (Sistedes)","author":"Gallardo M.-d.-M.","year":"2010","unstructured":"Gallardo , M.-d.-M. , and Panizo , L . An approach to verify hybrid systems with SPIN . In Procs. of PROLE 2010 (Sistedes) ( 2010 ). Gallardo, M.-d.-M., and Panizo, L. An approach to verify hybrid systems with SPIN. In Procs. of PROLE 2010 (Sistedes) (2010)."},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.5555\/788018.788803"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1006\/jcss.1998.1581"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2382756.2382793","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2382756.2382793","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:34:54Z","timestamp":1750239294000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2382756.2382793"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,11,27]]},"references-count":7,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2012,11,27]]}},"alternative-id":["10.1145\/2382756.2382793"],"URL":"https:\/\/doi.org\/10.1145\/2382756.2382793","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2012,11,27]]},"assertion":[{"value":"2012-11-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}