{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T14:37:42Z","timestamp":1712241462515},"reference-count":8,"publisher":"Association for Computing Machinery (ACM)","issue":"2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGCSE Bull."],"published-print":{"date-parts":[[2009,6,25]]},"abstract":"Formal methods were developed to provide systematic and rigorous techniques for software development, and they must be taught in the context of software engineering. In this paper, we discuss the importance of such a teaching paradigm and describe several specific techniques for teaching formal methods. These techniques have been tested over the last fifteen years in our formal methods education programs for undergraduate and graduate students at universities as well as practitioners at companies. We also present a curriculum to systematically introduce formal methods to students at university and a successful program of teaching formal methods to industry. Our experience shows that students can gain confidence in formal methods only when they learn their clear benefits in the context of software engineering.<\/jats:p>","DOI":"10.1145\/1595453.1595457","type":"journal-article","created":{"date-parts":[[2009,8,24]],"date-time":"2009-08-24T14:08:31Z","timestamp":1251122911000},"page":"17-23","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Teaching formal methods in the context of software engineering"],"prefix":"10.1145","volume":"41","author":[{"given":"Shaoying","family":"Liu","sequence":"first","affiliation":[{"name":"Hosei University, Tokyo, Japan"}]},{"given":"Kazuhiro","family":"Takahashi","sequence":"additional","affiliation":[{"name":"The Nippon Signal Co., Ltd., Saitama, Japan"}]},{"given":"Toshinori","family":"Hayashi","sequence":"additional","affiliation":[{"name":"The Nippon Signal Co., Ltd., Saitama, Japan"}]},{"given":"Toshihiro","family":"Nakayama","sequence":"additional","affiliation":[{"name":"The Nippon Signal Co., Ltd., Saitama, Japan"}]}],"member":"320","published-online":{"date-parts":[[2009,6,25]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Formal Engineering for Industrial Software Development Using the SOFL Method","author":"Liu S.","year":"2060","unstructured":"S. Liu . Formal Engineering for Industrial Software Development Using the SOFL Method . Springer-Verlag , ISBN 3-540- 2060 2-7, 2004. S. Liu. Formal Engineering for Industrial Software Development Using the SOFL Method. Springer-Verlag, ISBN 3-540-20602-7, 2004."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.663996"},{"issue":"2","key":"e_1_2_1_3_1","first-page":"103","article-title":"The Use of Software Engineering, Including the Z notation, in the Development of CICS","volume":"14","author":"Collins B.P.","year":"1988","unstructured":"B.P. Collins and C.J. Nix . The Use of Software Engineering, Including the Z notation, in the Development of CICS . Quality Assurance , 14 ( 2 ): 103 -- 110 , September 1988 . B.P. Collins and C.J. Nix. The Use of Software Engineering, Including the Z notation, in the Development of CICS. Quality Assurance, 14(2):103--110, September 1988.","journal-title":"Quality Assurance"},{"key":"e_1_2_1_4_1","first-page":"371","volume-title":"Software Fundamentals: Collected Papers by David L. Parnas","author":"Parnas D.L.","year":"2001","unstructured":"D.L. Parnas . Inspection of Safety-Critical Software Using Program-Function Tables . In D.M. Hoffman and D.M. Weiss, editors, Software Fundamentals: Collected Papers by David L. Parnas , pages 371 -- 382 . Addison Wesley , 2001 . D.L. Parnas. Inspection of Safety-Critical Software Using Program-Function Tables. In D.M. Hoffman and D.M. Weiss, editors, Software Fundamentals: Collected Papers by David L. Parnas, pages 371--382. Addison Wesley, 2001."},{"key":"e_1_2_1_5_1","first-page":"93","volume-title":"Proceedings of 2004 Symposium of Science and Technology on System Verification","author":"Sahara S.","year":"2004","unstructured":"S. Sahara . An Experience of Applying Formal Method on a Large Business Application (in Japanese) . In Proceedings of 2004 Symposium of Science and Technology on System Verification , pages 93 -- 100 , Osaka, Japan , Feb. 4-6 2004 . National Institute of Advanced Industrial Science and Technology (AIST). S. Sahara. An Experience of Applying Formal Method on a Large Business Application (in Japanese). In Proceedings of 2004 Symposium of Science and Technology on System Verification, pages 93--100, Osaka, Japan, Feb. 4-6 2004. National Institute of Advanced Industrial Science and Technology (AIST)."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.48796"},{"key":"e_1_2_1_7_1","volume-title":"Systematic Software Development Using VDM","author":"Jones C.B.","year":"1990","unstructured":"C.B. Jones . Systematic Software Development Using VDM . 2 nd edition, Prentice Hall , 1990 . C.B. Jones. Systematic Software Development Using VDM. 2nd edition, Prentice Hall, 1990.","edition":"2"},{"key":"e_1_2_1_8_1","volume-title":"Programming from Specifications","author":"Morgan C.","year":"1994","unstructured":"C. Morgan . Programming from Specifications . 2 nd edition, Prentice-Hall , 1994 . C. Morgan. Programming from Specifications. 2nd edition, Prentice-Hall, 1994.","edition":"2"}],"container-title":["ACM SIGCSE Bulletin"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1595453.1595457","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T07:47:00Z","timestamp":1672300020000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1595453.1595457"}},"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.1595457"],"URL":"https:\/\/doi.org\/10.1145\/1595453.1595457","relation":{},"ISSN":["0097-8418"],"issn-type":[{"value":"0097-8418","type":"print"}],"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"}}]}}