{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,8]],"date-time":"2023-01-08T10:50:02Z","timestamp":1673175002709},"reference-count":53,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Systems and Software"],"published-print":{"date-parts":[[2002,1]]},"DOI":"10.1016\/s0164-1212(01)00080-2","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T10:34:40Z","timestamp":1027593280000},"page":"59-82","source":"Crossref","is-referenced-by-count":2,"title":["Formal modeling in a commercial setting: A case study"],"prefix":"10.1016","volume":"60","author":[{"given":"Marsha","family":"Chechik","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andre","family":"Wong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0164-1212(01)00080-2_BIB1","unstructured":"Appendix I to Recommendation Z.100 \u2013 SDL Methodology Guidelines. CCITT, Geneva, 1993"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB2","doi-asserted-by":"crossref","unstructured":"Arts, T., Dam, M., 1999. Verifying a distributed database lookup manager written in Erlang. In: Wing, J., Woodcock, J. (Eds.), Proceedings of World Congress on Formal Methods in the Development of Computing Systems (FM'99), Lecture Notes in Computer Science, vol. 1708, Springer, Berlin, pp. 682\u2013700","DOI":"10.1007\/3-540-48119-2_38"},{"issue":"6","key":"10.1016\/S0164-1212(01)00080-2_BIB3","doi-asserted-by":"crossref","DOI":"10.1109\/52.636668","volume":"14","author":"Beckman","year":"1997","journal-title":"IEEE Software"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB4","doi-asserted-by":"crossref","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M., 1999. Meteor: a successful application of B in a large project. In: Wing, J., Woodcock, J. (Eds.), Proceedings of World Congress on Formal Methods in the Development of Computing Systems (FM'99), Lecture Notes in Computer Science, vol. 1708, Springer, Berlin, pp. 369\u2013387","DOI":"10.1007\/3-540-48119-2_22"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB5","series-title":"SDL with Applications from Protocol Specification","author":"Belina","year":"1991"},{"issue":"1","key":"10.1016\/S0164-1212(01)00080-2_BIB6","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/0164-1212(94)00054-Q","article-title":"The importance of ignorance in requirements engineering","volume":"28","author":"Berry","year":"1995","journal-title":"Journal of Systems and Software"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB7","series-title":"FME'96: Industrial Benefit and Advances in Formal Methods","first-page":"60","article-title":"Quantitative analysis of an application of formal methods","author":"Bicarregui","year":"1996"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB8","doi-asserted-by":"crossref","unstructured":"Bowen, J., Stavridou, V., 1993. The industrial take-up of formal methods in safety-critical and other areas: a perspective. In: Woodcock, J., Larsen, P. (Eds.), Proceedings of FME'93: Industrial Strength Formal Methods, Lecture Notes in Computer Science, vol. 670, Springer, Berlin","DOI":"10.1007\/BFb0024646"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB9","series-title":"FME'96: Industrial Benefit and Advances in Formal Methods","first-page":"214","article-title":"Formal and informal specifications of a secure system component: final results in a comparative study","author":"Brookes","year":"1996"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB10","doi-asserted-by":"crossref","unstructured":"Chaudron, M., Tretmans, J., Wijbrans, K., 1999. Lessons from the application of formal methods to the design of a storm surge barrier control system. In: Wing, J., Woodcock, J. (Eds.), Proceedings of World Congress on Formal Methods in the Development of Computing Systems (FM'99), Lecture Notes in Computer Science, vol. 1709, Springer, Berlin, pp. 1511\u20131526","DOI":"10.1007\/3-540-48118-4_30"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB11","unstructured":"Chechik, M., 1996. Automatic analysis of consistency between requirements and designs. PhD Thesis, University of Maryland, College Park, Maryland"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB12","unstructured":"Chechik, M., Wong, A., 1999. Formal methods when money is tight. In: Proceedings of the First Workshop on Economics-Driven Software Engineering Research (EDSER-1), Los Angeles (affiliated with ICSE-99)"},{"issue":"4","key":"10.1016\/S0164-1212(01)00080-2_BIB13","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/242223.242257","article-title":"Formal methods: state of the art and future directions","volume":"28","author":"Clarke","year":"1996","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB14","doi-asserted-by":"crossref","unstructured":"Conquet, E., Marty, J.-L., 1999. Formal design for automatic coding and testing: the ESSI\/SPACES project. In: Wing, J., Woodcock, J. (Eds.), Proceedings of World Congress on Formal Methods in the Development of Computing Systems (FM'99), Lecture Notes in Computer Science, vol. 1708, Springer, Berlin, pp. 57\u201375","DOI":"10.1007\/3-540-48119-2_6"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB15","doi-asserted-by":"crossref","unstructured":"Craigen, D., Gerhart, S., Ralston, T., 1993. An International Survey of Industrial Applications of Formal Methods, US National Institute of Standards and Technology","DOI":"10.1007\/978-1-4471-3556-2_1"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB16","unstructured":"Crow, J., Vito, B.D., 1996. Formalizing space shuttle software requirements. In: Workshop on Formal Methods in Software Practice, San Diego, CA"},{"issue":"1","key":"10.1016\/S0164-1212(01)00080-2_BIB17","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1109\/32.663994","article-title":"Experience using lightweight formal methods for requirements modeling","volume":"24","author":"Easterbrook","year":"1998","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB18","series-title":"SDL: Formal Object-Oriented Language for Communicating Systems","author":"Ellsberger","year":"1997"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB19","doi-asserted-by":"crossref","unstructured":"Facchi, C., Haubner, M., Hinkel, U., 1996. The SDL specification of the sliding window protocol revisited. Technical Report TUM-I9614, Technische Univerit\u00e4t M\u00fcnchen","DOI":"10.1016\/B978-044482816-3\/50034-4"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB20","unstructured":"Froberg, M., 1993. Automatic code generation from sdl to a declarative programming language. In: Proceedings of the Sixth SDL Forum, Darmstadt, Germany"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB21","doi-asserted-by":"crossref","unstructured":"Garbett, P., Parkes, J., Shackleton, M., Anderson, S., 1999. Secure synthesis of code: a process improvement experiment. In: Wing, J., Woodcock, J. (Eds.), Proceedings of World Congress on Formal Methods in the Development of Computing Systems (FM'99), Lecture Notes in Computer Science, vol. 1709, Springer, Berlin, pp. 1816\u20131835","DOI":"10.1007\/3-540-48118-4_46"},{"issue":"6","key":"10.1016\/S0164-1212(01)00080-2_BIB22","doi-asserted-by":"crossref","first-page":"582","DOI":"10.1109\/32.87283","article-title":"Why is software late? An empirical study of reasons for delay in software development?","volume":"17","author":"Genuchten","year":"1991","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB23","doi-asserted-by":"crossref","unstructured":"Gilham, F., Riemenschneider, R., Stavridou, V., 1999. Secure interoperation of secure distributed databases: an architecture verification case study. In: Wing, J., Woodcock, J. (Eds.), Proceedings of World Congress on Formal Methods in the Development of Computing Systems (FM'99), Lecture Notes in Computer Science, vol. 1708, Springer, Berlin, pp. 701\u2013717","DOI":"10.1007\/3-540-48119-2_39"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB24","unstructured":"Grasmanis, M., Medvedis, I., 1991. Approach to behaviour specification and automated test generation for telephone exchange systems. In: Proceedings of the Fifth SDL Forum, Glasgow, Scotland"},{"issue":"2","key":"10.1016\/S0164-1212(01)00080-2_BIB25","doi-asserted-by":"crossref","DOI":"10.1109\/52.506463","article-title":"Using formal methods to develop an ATC information system","volume":"13","author":"Hall","year":"1996","journal-title":"IEEE Software"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB26","doi-asserted-by":"crossref","unstructured":"Heimdahl, M.P., 1996. Lessons from the analysis of TCAS II. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA'96), San Diego, CA","DOI":"10.1145\/229000.226304"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB27","unstructured":"Hoare, J.P., 1995. Application of the B-method to CICS. In: Hinchey, M.G., Bowen, J.P. (Eds.), Applications of Formal Methods. Prentice-Hall International Series in Computer Science, pp. 97\u2013124"},{"issue":"4","key":"10.1016\/S0164-1212(01)00080-2_BIB28","first-page":"25","article-title":"An invitation to formal methods: impediments to industrial use of formal methods","volume":"29","author":"Holloway","year":"1996","journal-title":"IEEE Computer"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB29","unstructured":"ITU-T, 1993. ITU-T Recommendation Z.120: Message Sequence Chart (MSC). ITU-T"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB30","unstructured":"ITU-T, 1996. Specification and Description Language (SDL): ITU-T Recommendation Z.100. International Telecommunication Union"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB31","article-title":"Lightweight formal methods","author":"Jackson","year":"1996","journal-title":"IEEE Computer"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB32","unstructured":"Joannou, P.K., 1993. Experiences from application of digital systems in nuclear power plants. In: Proceedings of the Digital Systems Reliability and Nuclear Safety Workshop, Rockville, Maryland"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB33","doi-asserted-by":"crossref","unstructured":"King, S., Hammond, J., Chapman, R., Pryor, A., 1999. The value of verification: positive experience of industrial proof. In: Wing, J., Woodcock, J. (Eds.), Proceedings of World Congress on Formal Methods in the Development of Computing Systems (FM'99), Lecture Notes in Computer Science, vol. 1709, Springer, Berlin","DOI":"10.1007\/3-540-48118-4_31"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB34","unstructured":"Kooij, M., Provoost, L., 1998. Industrial report on the use of abstraction in SDL\/MSC. In: First Workshop of the SDL Forum Society on SDL and MSC, Berlin, Germany (ALCATEL)"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB35","unstructured":"Mansson, L., 1993. High level specification of a telecom application with SDL'92. In: Proceedings of the Sixth SDL Forum, Darmstadt, Germany"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB36","unstructured":"Mataga, P., Zave, P., 1995. Multiparadigm specification of an AT&T switching system. In: Hinchey, M.G., Bowen, J.P. (Eds.), Applications of Formal Methods. Prentice-Hall International Series in Computer Science, pp. 375\u2013398"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB37","doi-asserted-by":"crossref","unstructured":"McDermid, J., Golloway, A., Burton, S., Clark, J., Toyn, I., Tracey, N., Valentine, S., 1998. Towards industrially applicable formal methods: three small steps, and one giant leap. In: Proceedings of the Second International Conference on Formal Engineering Methods, pp. 76\u201388","DOI":"10.1109\/ICFEM.1998.730572"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB38","series-title":"Systems Engineering Using SDL-92","author":"Olsen","year":"1994"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB39","doi-asserted-by":"crossref","unstructured":"Parnas, D., 1993. Some theorems we should prove. In: Proceedings of 1993 International Conference on HOL Theorem Proving and its Applications. Vancouver, BC","DOI":"10.1007\/3-540-57826-9_132"},{"issue":"2","key":"10.1016\/S0164-1212(01)00080-2_BIB40","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1109\/2.566148","article-title":"Investigating the influence of formal methods","volume":"30","author":"Pfleeger","year":"1997","journal-title":"IEEE Computer"},{"issue":"5","key":"10.1016\/S0164-1212(01)00080-2_BIB41","doi-asserted-by":"crossref","DOI":"10.1109\/MS.1998.714869","article-title":"Can internet-based applications be engineered?","volume":"15","author":"Pressman","year":"1998","journal-title":"IEEE Software"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB42","doi-asserted-by":"crossref","unstructured":"Randimbivololona, F., Souyris, J., Baudin, P., Pacalet, A., Raguideau, K., Schoen, D., 1999. Applying formal proof techniques to avionics software: a pragmatic approach. In: Wing, J., Woodcock, J. (Eds.), Proceedings of World Congress on Formal Methods in the Development of Computing Systems (FM'99), Lecture Notes in Computer Science, vol. 1709, Springer, Berlin, pp. 1798\u20131815","DOI":"10.1007\/3-540-48118-4_45"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB43","first-page":"16","article-title":"An invitation to formal methods","author":"Saiedien","year":"1996","journal-title":"IEEE Computer"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB44","unstructured":"Sarma, A., 1989. Modeling broadband ISDN protocols with SDL. In: Proceedings of the Fifth SDL Forum. Glasgow, Scotland"},{"issue":"8","key":"10.1016\/S0164-1212(01)00080-2_BIB45","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1109\/2.707619","article-title":"Toward automatic detection of software failures","volume":"31","author":"Savor","year":"1998","journal-title":"IEEE Computer"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB46","unstructured":"Telelogic, 1998. Telelogic SDT home page. http:\/\/www.telelogic.com\/solution\/tools\/sdt.asp"},{"issue":"5","key":"10.1016\/S0164-1212(01)00080-2_BIB47","doi-asserted-by":"crossref","DOI":"10.1109\/2.675631","article-title":"Should computer scientists experiment more?","volume":"31","author":"Tichy","year":"1998","journal-title":"IEEE Computer"},{"issue":"6","key":"10.1016\/S0164-1212(01)00080-2_BIB48","doi-asserted-by":"crossref","DOI":"10.1109\/52.636594","article-title":"A missing link in software engineering","volume":"14","author":"Tockey","year":"1997","journal-title":"IEEE Software"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB49","unstructured":"Vgel, H., Kellerer, W., Karg, S., Kober, M., Beckert, A., Einfalt, G., 1998. SDL based prototyping of ISDN-DECT-PBX switching software. In: First Workshop of the SDL Forum Society on SDL and MSC, Berlin, Germany"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB50","doi-asserted-by":"crossref","unstructured":"Weber-Wulff, D., 1993. Selling formal methods to industry. In: Woodcock, J., Larsen, P. (Eds.), Proceedings of FME'93: Industrial Benefit of Formal Methods, First International Symposium of Formal Methods Europe, Odense, Denmark, Springer, Berlin, pp. 671\u2013678","DOI":"10.1007\/BFb0024673"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB51","unstructured":"Wong, A., 1998. The diary of the formal-method survey. http:\/\/www.cs.toronto.edu\/\u223candre\/progress.html"},{"key":"10.1016\/S0164-1212(01)00080-2_BIB52","unstructured":"Wong, A., 1999. Formalizing requirements in a commercial setting: a case study. Master's Thesis, University of Toronto, Department of Computer Science, Toronto, ON, Canada"},{"issue":"5","key":"10.1016\/S0164-1212(01)00080-2_BIB53","doi-asserted-by":"crossref","DOI":"10.1109\/2.675630","article-title":"Experimental models for validating technology","volume":"31","author":"Zelkowitz","year":"1998","journal-title":"IEEE Computer"}],"container-title":["Journal of Systems and Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0164121201000802?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0164121201000802?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T03:28:20Z","timestamp":1578454100000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0164121201000802"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,1]]},"references-count":53,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,1]]}},"alternative-id":["S0164121201000802"],"URL":"https:\/\/doi.org\/10.1016\/s0164-1212(01)00080-2","relation":{},"ISSN":["0164-1212"],"issn-type":[{"value":"0164-1212","type":"print"}],"subject":[],"published":{"date-parts":[[2002,1]]}}}