{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:35:02Z","timestamp":1750307702478,"version":"3.41.0"},"reference-count":8,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2009,6,25]],"date-time":"2009-06-25T00:00:00Z","timestamp":1245888000000},"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":["SIGCSE Bull."],"published-print":{"date-parts":[[2009,6,25]]},"abstract":"<jats:p>This paper is the preliminary report of a joint research project on developing a body of knowledge on model checking. The project is being carried out by four organizations that give model checking courses to software engineers in Japan. The paper explains the main objective of the project and reports the results of an evaluation of model checking programs.<\/jats:p>","DOI":"10.1145\/1595453.1595461","type":"journal-article","created":{"date-parts":[[2009,8,24]],"date-time":"2009-08-24T14:08:31Z","timestamp":1251122911000},"page":"45-50","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Model checking education for software engineers in Japan"],"prefix":"10.1145","volume":"41","author":[{"given":"Hideaki","family":"Nishihara","sequence":"first","affiliation":[{"name":"Research Center for Verification and Semantics National Institute of Advanced Industrial Science and Technology (AIST), Osaka, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Koichi","family":"Shinozaki","sequence":"additional","affiliation":[{"name":"The Kansai Electric Power Co., Inc., Hyogo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Koji","family":"Hayamizu","sequence":"additional","affiliation":[{"name":"Melco Power Systems Co., Ltd., Kobe-shi, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toshiaki","family":"Aoki","sequence":"additional","affiliation":[{"name":"Research Center for Trustworthy e-Society Japan Advanced Institute of Science and Technology, Ishikawa, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kenji","family":"Taguchi","sequence":"additional","affiliation":[{"name":"Grace Center, Information Systems Architecture Research Division National Institute of Informatics, Chiyoda-ku, Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fumihiro","family":"Kumeno","sequence":"additional","affiliation":[{"name":"Mitsubishi Research Institute, Inc., Chiyoda-ku, Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,6,25]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"ISO\/IEC","author":"IEC","year":"2005","unstructured":"ISO\/ IEC 15408. Information technology - Security techniques - Evaluation criteria for IT security -- Part1, Part2 and Part3 . ISO\/IEC , 2005 . ISO\/IEC 15408. Information technology - Security techniques - Evaluation criteria for IT security -- Part1, Part2 and Part3. ISO\/IEC, 2005."},{"key":"e_1_2_1_2_1","volume-title":"Functional safety of electrical\/ electronic\/ programmable electronic safety related systems -- Part3: Software requirements","author":"IEC","year":"1998","unstructured":"IEC 61508-3. Functional safety of electrical\/ electronic\/ programmable electronic safety related systems -- Part3: Software requirements . Bureau Central de la Commission Electrotechnique International, 1998 . IEC 61508-3. Functional safety of electrical\/ electronic\/ programmable electronic safety related systems -- Part3: Software requirements. Bureau Central de la Commission Electrotechnique International, 1998."},{"key":"e_1_2_1_3_1","volume-title":"Guide to the Software Engineering Body of Knowledge 2004 Version SWEBOK","author":"Abran A.","year":"2004","unstructured":"A. Abran , J. W. Moore , P. Bourque , and R. Dupuis . Guide to the Software Engineering Body of Knowledge 2004 Version SWEBOK . IEEE , 2004 . A. Abran, J. W. Moore, P. Bourque, and R. Dupuis. Guide to the Software Engineering Body of Knowledge 2004 Version SWEBOK. IEEE, 2004."},{"key":"e_1_2_1_4_1","volume-title":"The SPIN model checker: Primer and reference manual","author":"Holzmann G.J.","year":"2004","unstructured":"G.J. Holzmann . The SPIN model checker: Primer and reference manual . Addison Wesley , 2004 . G.J. Holzmann. The SPIN model checker: Primer and reference manual. Addison Wesley, 2004."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.89"},{"key":"e_1_2_1_6_1","volume-title":"Concurrency: State Models &amp","author":"Magee J.","year":"2006","unstructured":"J. Magee and J. Kramer . Concurrency: State Models &amp ; Java Programs, Second Edition . John Wiley & amp; Sons, 2006 . J. Magee and J. Kramer. Concurrency: State Models &amp; Java Programs, Second Edition. John Wiley &amp; Sons, 2006."},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"McMillan K.L.","year":"1993","unstructured":"K.L. McMillan . Symbolic Model Checking . Kluwer Academic Publishers , Norwell, MA, USA , 1993 . K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell, MA, USA, 1993."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"J.N.\n      Oliveira\n    .\n  A survey of formal methods courses in European higher education\n  . In C. Neville Dean and Raymond T. Boute editors TFM volume \n  3294\n   of \n  Lecture Notes in Computer Science pages \n  235\n  --\n  248\n  . \n  Springer 2004\n  .  J.N. Oliveira. A survey of formal methods courses in European higher education. In C. Neville Dean and Raymond T. Boute editors TFM volume 3294 of Lecture Notes in Computer Science pages 235--248. Springer 2004.","DOI":"10.1007\/978-3-540-30472-2_16"}],"container-title":["ACM SIGCSE Bulletin"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1595453.1595461","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1595453.1595461","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:03Z","timestamp":1750253403000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1595453.1595461"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,6,25]]},"references-count":8,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,6,25]]}},"alternative-id":["10.1145\/1595453.1595461"],"URL":"https:\/\/doi.org\/10.1145\/1595453.1595461","relation":{},"ISSN":["0097-8418"],"issn-type":[{"type":"print","value":"0097-8418"}],"subject":[],"published":{"date-parts":[[2009,6,25]]},"assertion":[{"value":"2009-06-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}