{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,2]],"date-time":"2024-03-02T22:00:29Z","timestamp":1709416829736},"reference-count":54,"publisher":"IGI Global","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011,4,1]]},"abstract":"

Introduction of formal model-based practices into the development process of a product in a company implicates changes in the verification and validation activities. A testing process that focuses only on code is not comprehensive in a framework where the building blocks of development are models, and industry is currently heading toward more effective strategies to cope with this new reality. This paper reports the experience of a railway signalling manufacturer in changing its unit level verification process from code-based testing to a two-step approach comprising model-based testing and abstract interpretation. Empirical results on different projects, on which the overall development process was progressively tuned, show that the change paid back in terms of verification cost reduction (about 70%), bug detection, and correction capability.<\/p>","DOI":"10.4018\/jertcs.2011040103","type":"journal-article","created":{"date-parts":[[2011,10,19]],"date-time":"2011-10-19T16:18:53Z","timestamp":1319041133000},"page":"42-61","source":"Crossref","is-referenced-by-count":6,"title":["Adoption of Model-Based Testing and Abstract Interpretation by a Railway Signalling Manufacturer"],"prefix":"10.4018","volume":"2","author":[{"given":"Alessio","family":"Ferrari","sequence":"first","affiliation":[{"name":"University of Florence, D.S.I., Italy"}]},{"given":"Gianluca","family":"Magnani","sequence":"additional","affiliation":[{"name":"General Electric Transportation Systems, Italy"}]},{"given":"Daniele","family":"Grasso","sequence":"additional","affiliation":[{"name":"General Electric Transportation Systems, Italy"}]},{"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[{"name":"University of Florence, D.S.I., Italy"}]},{"given":"Matteo","family":"Tempestini","sequence":"additional","affiliation":[{"name":"General Electric Transportation Systems, Italy"}]}],"member":"2432","reference":[{"key":"jertcs.2011040103-0","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00007-6"},{"key":"jertcs.2011040103-1","doi-asserted-by":"crossref","unstructured":"Aydal, E. G., Paige, R. F., Utting, M., & Woodcock, J. (2009). Putting formal specifications under the magnifying glass: Model-based testing for validation. In Proceedings of the 2nd International Conference on Software Testing Verification and Validation, Denver, CO (pp. 131-140). Washington, DC: IEEE Computer Society.","DOI":"10.1109\/ICST.2009.20"},{"key":"jertcs.2011040103-2","doi-asserted-by":"crossref","unstructured":"Bacherini, S., Fantechi, A., Tempestini, M., & Zingoni, N. (2006). A story about formal methods adoption by a railway signaling manufacturer. In J. Misra, T. Nipkow, & E. Sekerinski (Eds.), Proceedings of the 14th International Symposium on Formal Methods, Hamilton, ON, Canada (LNCS 4085, pp. 179-189).","DOI":"10.1007\/11813040_13"},{"key":"jertcs.2011040103-3","unstructured":"Baresel, A., Conrad, M., Sadeghipour, S., & Wegener, J. (2003). The interplay between model coverage and code coverage. In Proceedings of the 11th European International Conference on Software Testing, Analysis and Review, Amsterdam, Netherlands."},{"key":"jertcs.2011040103-4","doi-asserted-by":"crossref","unstructured":"Barkah, D., Ermedahl, A., Gustafsson, J., Lisper, B., & Sandberg, C. (2008). Evaluation of automatic flow analysis for WCET calculation on industrial real-time system code. In Proceedings of the 20th Euromicro Conference on Real-Time Systems, Prague, Czech Republic (pp. 331-340). Washington, DC: IEEE Computer Society.","DOI":"10.1109\/ECRTS.2008.37"},{"key":"jertcs.2011040103-5","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, R., Mauborgne, R., Min\u00e9, A., et al. (2003). A static analyzer for large safety-critical software. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, San Diego, CA (pp. 196-207). New York, NY: ACM Press.","DOI":"10.1145\/780822.781153"},{"key":"jertcs.2011040103-6","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00017-9"},{"key":"jertcs.2011040103-7","unstructured":"Brat, G., & Klemm, R. (2003). Static analysis of the mars exploration rover flight software. In Proceedings of the 1st International Space Mission Challenges for Information Technology, Pasadena, CA (pp. 321-326). Washington, DC: IEEE Computer Society."},{"key":"jertcs.2011040103-8","doi-asserted-by":"crossref","unstructured":"Broy, M., & Jonsson, B. Katoen, Philipps, J., Leucker, M., & Pretschner, A. (eds.). (2005). Model-based testing of reactive systems (LNCS 3472, pp. 281-291). Berlin, Germany: Springer-Verlag.","DOI":"10.1007\/b137241"},{"key":"jertcs.2011040103-9","unstructured":"Comit\u00e9 Europ\u00e9en de Normalisation en \u00c9lectronique et en \u00c9lectrotechnique. (1999). EN 50126: Railway applications - the specification and demonstration of dependability, reliability, availability, maintainability and safety (RAMS) (Tech. Rep. No. TX9X). Brussels, Belgium: CENELEC."},{"key":"jertcs.2011040103-10","year":"2001","journal-title":"EN 50128: Railway applications - communications, signalling and processing systems - software for railway control and protection systems"},{"key":"jertcs.2011040103-11","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0082-0"},{"key":"jertcs.2011040103-12","doi-asserted-by":"crossref","unstructured":"Cousot, P., & Cousot, R. (1977). Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Los Angeles, CA (pp.238-353). New York, NY: ACM Press.","DOI":"10.1145\/512950.512973"},{"key":"jertcs.2011040103-13","doi-asserted-by":"crossref","unstructured":"Cousot, P., & Cousot, R. (1979). Systematic design of program analysis frameworks. In Proceedings of the 6th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX (pp. 269-282). New York, NY: ACM Press.","DOI":"10.1145\/567752.567778"},{"key":"jertcs.2011040103-14","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"jertcs.2011040103-15","doi-asserted-by":"crossref","unstructured":"Dalal, S. R., Jain, A., Karunanithi, N., Leaton, J. M., Lott, C. M., Patton, G. C., et al. (1999). Model-based testing in practice. In Proceedings of the 21st International Conference on Software Engineering, Los Angeles, CA (pp. 285-294). New York, NY: ACM Press.","DOI":"10.1145\/302405.302640"},{"key":"jertcs.2011040103-16","doi-asserted-by":"crossref","unstructured":"Delmas, D., & Souyris, J. (2007). Astr\u00e9e: From research to industry. In H. R. Nielson & G. Fil\u00e9 (Eds.), Proceedings of the 14th International Static Analysis Symposium, Lyngby, Denmark (LNCS 4634, pp. 437-451).","DOI":"10.1007\/978-3-540-74061-2_27"},{"key":"jertcs.2011040103-17","unstructured":"Deutsch, A. (2004). Static verification of dynamic properties. Retrieved from http:\/\/www.sigada.org\/conf\/sigada2003\/SIGAda2003-CDROM"},{"key":"jertcs.2011040103-18","first-page":"825","article-title":"Model-based software testing","volume":"Vol. 1","author":"I. K.El-Far","year":"2002","journal-title":"Encyclopedia of software engineering"},{"key":"jertcs.2011040103-19","unstructured":"Ferdinand, C., Heckmann, R., & Franzel, B. (2007). Static memory and timing analysis of embedded systems code. In Proceedings of the 3rd European Symposium on Verification and Validation of Software Systems, Eindhoven, The Netherlands (pp. 153-163)."},{"key":"jertcs.2011040103-20","unstructured":"Ferrari, A., Fantechi, A., Tempestini, M., & Zingoni, N. (2009). Modeling guidelines for code generation in the railway signaling context. In Proceedings of the 1st NASA Formal Methods Symposium, Moffet Field, CA (pp. 166-170)."},{"key":"jertcs.2011040103-21","doi-asserted-by":"crossref","unstructured":"Ferrari, A., Grasso, D., Magnani, G., Fantechi, A., & Tempestini, M. (2010, September). The Metr\u00f4 Rio ATP case study. In S. Kowalewski & M. Roveri (Eds.), Proceedings of the 15th International Workshop on Formal Methods for Industrial Critical Systems, Antwerp, Belgium (LNCS 6371, pp. 1-16).","DOI":"10.1007\/978-3-642-15898-8_1"},{"key":"jertcs.2011040103-22","doi-asserted-by":"publisher","DOI":"10.1145\/356674.356676"},{"key":"jertcs.2011040103-23","doi-asserted-by":"crossref","unstructured":"Grasso, D., Fantechi, A., Ferrari, A., Becheri, C., & Bacherini, S. (2010). Model based testing and abstract interpretation in the railway signaling context. In Proceedings of the Third International Conference on Software Testing, Verification and Validation, Paris, France (pp. 103-106). Washington, DC: IEEE Computer Society.","DOI":"10.1109\/ICST.2010.44"},{"key":"jertcs.2011040103-24","doi-asserted-by":"crossref","unstructured":"Gulavani, B. S., & Rajamani, S. K. (2006). Counterexample driven refinement for abstract interpretation. In H. Hermanns & J. Palsberg (Eds.), Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Wien, Austria (LNCS 3920, pp. 474-488).","DOI":"10.1007\/11691372_34"},{"key":"jertcs.2011040103-25","unstructured":"Harel, D., Lachover, H., Naamad, A., Pnueli, A., Politi, M., Sherman, R., et al. (1988). Statemate: A working environment for the development of complex reactive systems. In Proceedings of the 10th International Conference on Software Engineering, Raffles City, Singapore (pp. 396-496). Washington, DC: IEEE Computer Society."},{"key":"jertcs.2011040103-26","doi-asserted-by":"crossref","unstructured":"Hessel, A., & Pettersson, P. (2006). Model-based testing of a WAP gateway: An industrial study. In L. Brim & M. Leucker (Eds.), Proceedings of the 11th International Workshop on Formal Methods for Industrial Critical Systems, Bonn, Germany (LNCS 4346, pp. 116-131).","DOI":"10.1007\/978-3-540-70952-7_8"},{"key":"jertcs.2011040103-27","doi-asserted-by":"publisher","DOI":"10.1145\/1459352.1459354"},{"key":"jertcs.2011040103-28","unstructured":"Hierons, R. M., Bowen, J. P., & Harman, M. (Eds.). (2008). Formal methods and testing (LNCS 4949, pp. 1-38). Berlin, Germany: Springer-Verlag."},{"key":"jertcs.2011040103-29","doi-asserted-by":"publisher","DOI":"10.1109\/T-C.1975.224259"},{"key":"jertcs.2011040103-30","doi-asserted-by":"crossref","unstructured":"Jung, Y., Kim, J., Shin, J., & Yi, K. (2005). Taming false alarms from a domain-unaware c analyzer by a Bayesian statistical post analysis. In C. Hankin & I. Siveroni (Eds.), Proceedings of the 12th International Static Analysis Symposium, London, UK (LNCS 3672, pp. 203-217).","DOI":"10.1007\/11547662_15"},{"key":"jertcs.2011040103-31","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2009.10.004"},{"key":"jertcs.2011040103-32","doi-asserted-by":"crossref","unstructured":"Kremenek, T., & Engler, D. R. (2003). Z-Ranking: Using statistical analysis to counter the impact of static analysis approximations. In R. Cousot (Ed.), Proceedings of the 10th International Static Analysis Symposium, San Diego, CA (LNCS 2694, pp. 295-315).","DOI":"10.1007\/3-540-44898-5_16"},{"key":"jertcs.2011040103-33","doi-asserted-by":"crossref","unstructured":"Larsen, K. G., Mikucionis, M., Nielsen, B., & Skou, A. (2005). Testing real-time embedded software using UPPAAL-TRON - an industrial case study. In Proceedings of the 5th ACM International Conference on Embedded Software, Jersey City, NJ (pp. 299-306). New York, NY: ACM Press.","DOI":"10.1145\/1086228.1086283"},{"key":"jertcs.2011040103-34","unstructured":"Matlab Automotive Advisory Board. (2007). Control algorithm modeling guidelines using Matlab, Simulink and Stateflow, version 2.0. Retrieved from http:\/\/www.mathworks.com\/automotive\/standards\/maab.html;jsessionid=WTtvNL6XcCkNpFBMJQsPdQ6tnhcNsPQXJx9Jxffh1rLDnTBKKh7w!892165066"},{"key":"jertcs.2011040103-35","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646372"},{"key":"jertcs.2011040103-36","doi-asserted-by":"crossref","unstructured":"Mohagheghi, P., & Dehlen, V. (2010). Where is the proof? A review of experiences from applying MDE in industry. In I. Schieferdecker & A. Hartman (Eds.), Proceedings of the International Conference on Model Based Testing of Reactive Systems (LNCS 5095, pp. 432-443).","DOI":"10.1007\/978-3-540-69100-6_31"},{"key":"jertcs.2011040103-37","unstructured":"Object Management Group. (2010a). OMG systems modeling language (OMG SysML\u2122), Version 1.2. Retrieved from http:\/\/www.omg.org\/spec\/SysML\/1.2"},{"key":"jertcs.2011040103-38","unstructured":"Object Management Group. (2010b). OMG unified modeling language\u2122(OMG UML), Infrastructure, Version 2.3. Retrieved from http:\/\/www.omg.org\/spec\/UML\/2.3\/Infrastructure"},{"key":"jertcs.2011040103-39","unstructured":"Object Management Group. (2010c). OMG unified modeling language\u2122(OMG UML), Superstructure, Version 2.3. Retrieved from http:\/\/www.omg.org\/spec\/UML\/2.3\/Superstructure"},{"key":"jertcs.2011040103-40","doi-asserted-by":"crossref","unstructured":"Pasareanu, C. S., Schumann, J., Mehlitz, P., Lowry, M., Karsai, G., Nine, H., et al. (2009). Model based analysis and test generation for flight software. In Proceedings of the 3rd IEEE International Conference on Space Mission Challenges for Information Technology, Pasadena, CA (pp. 83-90). Washington, DC: IEEE Computer Society.","DOI":"10.1109\/SMC-IT.2009.18"},{"key":"jertcs.2011040103-41","doi-asserted-by":"crossref","unstructured":"Post, H., & Sinz, C. Kaiser, A., & Gorges, T. (2008). Reducing false positives by combining abstract interpretation and bounded model checking. In Proceedings of the 23rd IEEE\/ACM International Conference on Automated Software Engineering, L\u2019Aquila, Italy (pp. 188-197). Washington, DC: IEEE Computer Society.","DOI":"10.1109\/ASE.2008.29"},{"key":"jertcs.2011040103-42","doi-asserted-by":"crossref","unstructured":"Prenninger, W., El-Ramly, M., & Horstmann, M. (2005). Case studies. In M. Broy, B. Jonsson, J. P. Katoen, M. Leucker, & A. Pretschner (Eds.), Proceedings of the International Conference on Model Based Testing of Reactive Systems (LNCS 3472, pp. 439-461).","DOI":"10.1007\/11498490_19"},{"key":"jertcs.2011040103-43","doi-asserted-by":"crossref","unstructured":"Pretschner, A., & Phillips, J. (2005). Methodological issues in model-based testing. In M. Broy, B. Jonsson, J. P. Katoen, M. Leucker, & A. Pretschner (Eds.), Proceedings of the International Conference on Model Based Testing of Reactive Systems (LNCS 3472, pp. 281-291).","DOI":"10.1007\/11498490_13"},{"key":"jertcs.2011040103-44","doi-asserted-by":"crossref","unstructured":"Pretschner, A., Prenninger, W., Wagner, S., K\u00fchnel, C., Baumgartner, M., Sostawa, B., et al. (2005). One evaluation of model-based testing and its automation. In Proceedings of the 27th International Conference on Software Engineering, St. Louis, MO (pp. 392-401). New York, NY: ACM Press.","DOI":"10.1145\/1062455.1062529"},{"key":"jertcs.2011040103-45","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-003-0128-3"},{"key":"jertcs.2011040103-46","doi-asserted-by":"publisher","DOI":"10.1145\/1113830.1113833"},{"key":"jertcs.2011040103-47","doi-asserted-by":"crossref","unstructured":"Rival, X. (2005). Understanding the origin of alarms in Astr\u00e9e. In C. Hankin & I. Siveroni (Eds), Proceedings of the 12th International Static Analysis Symposium, London, UK (LNCS 3672, pp. 303-319).","DOI":"10.1007\/11547662_21"},{"key":"jertcs.2011040103-48","unstructured":"Streitferdt, D., Nenninger, P., Bilich, C., Kantz, F., Bauer, T., & Eschbach, R. (2008). Model-based testing in the automation domain, safety enabled. In Proceedings of the 1st Workshop on Model-based Testing in Practice, Berlin, Germany (pp. 83-89)."},{"key":"jertcs.2011040103-49","unstructured":"Thesing, S., Souyris, J., Heckmann, R., Randimbivololona, F., Langenbach, M., Wilhelm, R., et al. (2003). An abstract interpretation-based timing validation of hard real-time avionics software systems. In Proceedings of the International Conference on Dependable Systems and Networks, San Francisco, CA (pp. 625-632).Washington, DC: IEEE Computer Society."},{"key":"jertcs.2011040103-50","author":"M.Utting","year":"2007","journal-title":"Practical model-based testing: A tools approach"},{"key":"jertcs.2011040103-51","doi-asserted-by":"crossref","unstructured":"Venet, A., & Brat, G. (2004). Precise and efficient static array bound checking for large embedded C programs. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, Washington, DC (pp. 231-242). New York, NY: ACM Press.","DOI":"10.1145\/996893.996869"},{"key":"jertcs.2011040103-52","doi-asserted-by":"publisher","DOI":"10.1016\/0950-5849(90)90044-R"},{"key":"jertcs.2011040103-53","unstructured":"Weiser, M. (1981). Program slicing. In Proceedings of the 5th International Conference on Software Engineering, San Diego, CA (pp. 439-449). Washington, DC: IEEE Computer Society."}],"container-title":["International Journal of Embedded and Real-Time Communication Systems"],"original-title":[],"language":"ng","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=54248","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T20:00:22Z","timestamp":1654113622000},"score":1,"resource":{"primary":{"URL":"https:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/jertcs.2011040103"}},"subtitle":[""],"short-title":[],"issued":{"date-parts":[[2011,4,1]]},"references-count":54,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,4]]}},"URL":"https:\/\/doi.org\/10.4018\/jertcs.2011040103","relation":{},"ISSN":["1947-3176","1947-3184"],"issn-type":[{"value":"1947-3176","type":"print"},{"value":"1947-3184","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,4,1]]}}}