{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:45:26Z","timestamp":1743072326632,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319174037"},{"type":"electronic","value":"9783319174044"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17404-4_7","type":"book-chapter","created":{"date-parts":[[2015,4,16]],"date-time":"2015-04-16T08:45:59Z","timestamp":1429173959000},"page":"97-110","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Using Alloy in Introductory Courses of Formal Methods"],"prefix":"10.1007","author":[{"given":"Shin","family":"Nakajima","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,4,17]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book - Assgining Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book - Assgining Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: Formal methods in industry - achievements, problems, future. In: Proceedings of ICSE 2006, pp. 761\u2013767 (2006)","DOI":"10.1145\/1134285.1134406"},{"key":"7_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B - System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"issue":"3","key":"7_CR4","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/BF01214918","volume":"8","author":"R-J Back","year":"1995","unstructured":"Back, R.-J., Sere, K.: Superposition refinement of reactive systems. Formal Aspects Comput. 8(3), 324\u2013346 (1995)","journal-title":"Formal Aspects Comput."},{"key":"7_CR5","volume-title":"Principles of Concurrent and Distributed Programming","author":"M Ben-Ari","year":"2006","unstructured":"Ben-Ari, M.: Principles of Concurrent and Distributed Programming, 2nd edn. Addison-Wesley, Boston (2006)","edition":"2"},{"key":"7_CR6","volume-title":"Software Engineering (three volumes)","author":"D Bj\u00f8rner","year":"2006","unstructured":"Bj\u00f8rner, D.: Software Engineering (three volumes). Springer, Berlin (2006)"},{"key":"7_CR7","first-page":"23","volume":"137","author":"C Bolton","year":"2005","unstructured":"Bolton, C.: Using the alloy analyzer to verify data refinement in Z. ENTCS 137, 23\u201344 (2005)","journal-title":"ENTCS"},{"issue":"1","key":"7_CR8","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Dick, J., Faivre, A.: Automating the generation and sequencing of test cases from model-based specifications. In: Proceedings of FME\u201993, pp. 268\u2013284 (1993)","DOI":"10.1007\/BFb0024651"},{"issue":"10","key":"7_CR10","doi-asserted-by":"publisher","first-page":"859","DOI":"10.1145\/355604.361591","volume":"15","author":"EW Dijkstra","year":"1972","unstructured":"Dijkstra, E.W.: The humble programmer - ACM turing award lecture. Commun. ACM 15(10), 859\u2013866 (1972)","journal-title":"Commun. ACM"},{"key":"7_CR11","volume-title":"Design Patterns - Elements of Reusable Object-Oriented Software","author":"E Gamma","year":"1995","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns - Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"He, J., Hoare, C.A.R., Sanders, J.W.: Date refinement refined - resume. In: Proceedings of ESOP\u201986, pp. 187\u2013196 (1986)","DOI":"10.1007\/3-540-16442-1_14"},{"key":"7_CR13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science","author":"M Huth","year":"2004","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science, 2nd edn. Cambridge University Press, Cambridge (2004)","edition":"2"},{"key":"7_CR14","unstructured":"Jackson, D., Wing, J.: Lightweight formal methods. In: Saidian, H. (ed.) An Invitation to Formal Methods, IEEE Computer (1996)"},{"key":"7_CR15","volume-title":"Software Abstractions - Logic, Language, and Analysis, revised edn","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions - Logic, Language, and Analysis, revised edn. The MIT Press, London (2012)"},{"key":"7_CR16","volume-title":"Systematic Software Development with VDM","author":"C Jones","year":"1990","unstructured":"Jones, C.: Systematic Software Development with VDM, 2nd edn. Prentice Hall, New York (1990)","edition":"2"},{"key":"7_CR17","unstructured":"Jones, C.: A rigorous approach to formal methods. In: Saidian, A. (ed.) An Invitation to Formal Methods, IEEE Computer (1996)"},{"issue":"4","key":"7_CR18","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1145\/1232743.1232745","volume":"50","author":"J Kramer","year":"2007","unstructured":"Kramer, J.: Is abstraction the key to computing? Comm. ACM 50(4), 37\u201342 (2007)","journal-title":"Comm. ACM"},{"key":"7_CR19","volume-title":"Learning by Doing: Practical Courses in Lightweight Formal Methods using VDM++, CS-TR-992","author":"PG Larsen","year":"2006","unstructured":"Larsen, P.G., Fitzgerald, J.S., Riddle, S.: Learning by Doing: Practical Courses in Lightweight Formal Methods using VDM++, CS-TR-992. University Newcastle upon Tyne, Tyne (2006)"},{"key":"7_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07287-5","volume-title":"Formal Engineering for Industrial Software Development using the SOFL Method","author":"S Liu","year":"2004","unstructured":"Liu, S.: Formal Engineering for Industrial Software Development using the SOFL Method. Springer, Edinburgh (2004)"},{"key":"7_CR21","volume-title":"Concurrency - State Models & Java Programming","author":"J Magee","year":"2006","unstructured":"Magee, J., Kramer, J.: Concurrency - State Models & Java Programming, 2nd edn. Wiley, Chichester (2006)","edition":"2"},{"key":"7_CR22","unstructured":"Nakajima, S.: Introduction to Formal Methods - Logic-Based Software Development Methods (in Japanese), Ohm-sya (2012)"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-04912-5_3","volume-title":"Teaching Formal Methods","author":"PC \u00d6lveczky","year":"2009","unstructured":"\u00d6lveczky, P.C.: Teaching formal methods based on rewriting logic and maude. In: Gibbons, J., Oliveira, J.N. (eds.) TFM 2009. LNCS, vol. 5846, pp. 20\u201338. Springer, Heidelberg (2009)"},{"issue":"2","key":"7_CR24","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"MR Prasad","year":"2005","unstructured":"Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. J. STTT 7(2), 156\u2013173 (2005)","journal-title":"J. STTT"},{"key":"7_CR25","unstructured":"Shaw, M.: Whither software engieering education?, an invited talk at IEEE CSEE&T 2011, Honolulu (2011)"},{"key":"7_CR26","volume-title":"The Z Notation - A Reference Manual","author":"JM Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation - A Reference Manual. Prentice Hall, Englewood Cliffs (1992)"},{"key":"7_CR27","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1109\/2.58215","volume":"23","author":"J Wing","year":"1990","unstructured":"Wing, J.: A Specifier\u2019s Introduction to Formal Methods. IEEE Comput. 23, 8\u201324 (1990)","journal-title":"IEEE Comput."},{"key":"7_CR28","volume-title":"Using Z - Specification, Refinement, and Proof","author":"JCP Woodcock","year":"1996","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z - Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)"}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17404-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,20]],"date-time":"2023-01-20T07:02:05Z","timestamp":1674198125000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17404-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319174037","9783319174044"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17404-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"17 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}