Department of Information Technology

Model Learning

Model-based Design is an increasingly important method for software development, e.g., for particular embedded and networking applications. It is based on pervasive use of models for all software development activities, including specification, implementation, verification, and testing. A key impediment is that it requires significant up-front effort to create models and maintain them as the software evolves. The goal of Model Learning is to develop automated techniques for generating models of software components automatically, typically from information obtained by performing large test suites. The overall goal is that such techniques should be readily applicable to components in e.g., embedded and networked systems. Our work focuses on generating state machine models, extended with facilities to model data manipulation and nonfunctional properties.

Our starting point is existing techniques for black-box learning of finite automata and state machines, such as the L* algorithm, which allow to construct finite-state models from the results of test suites. One of our major goals is to extend these techniques so that they become applicable to realistic systems, in particular so that they can also model data manipulation and timing properties.

Achievements

  • A black-box active learning algorithm, called SL*, for learning extended finite state machines (EFSM)s by black-box testing. EFSMs can model both data flow and control behavior of software components.
    • SL* is based on an interesting generalization of classic automata theory to handle infinite alphabets, where symbols contain values from some data domain. Such alphabets can represent, e.g., messages and method calls, including data parameters, in models of component behavior.
    • SL* is implemented in RALIB
  • We have also initiate another approach for learning EFSMs, based on combining abstraction with automata learning. This approach has been further developed by the group of Frits Vaandrager at Nijmegen univerisity
  • A general technique to specify coverage criteria in model-based test generation (FATES04)

Publications

  • Active Learning for Extended Finite State Machines. S. Cassel, F. Howar, B. Jonsson, B. Steffen. Formal Aspects of Computing, 28(2): 233-263 (2016). (DOI, preliminary version as Technical Report 2015-032
  • Industrial Evaluation of Test Suite Generation Strategies for Model-Based Testing J. Blom, B. Jonsson, S.-O. Nyström, in A-MOST 2016: 12th Advances in Model based Testing Workshop, Chicago, April 11, 2016, Electronic Edition [author version],
  • Generating Models of Infinite-State Communication Protocols Using Regular Inference with Abstraction F. Aarts, B. Jonsson, J. Uijen, F.W. Vaandrager. Formal Methods in System Design, 46(1):1-41, 2015. DOI, earlier version as Technical report ICIS-R13001, Radboud University Nijmegen, January 2013
  • A Succinct Canonical Register Automaton Model S. Cassel, F. Howar, B. Jonsson, M. Merten, B. Steffen. Journal of Logic and Algebraic Programming 84(1): 54-66, Elsevier, Jan. 2015. DOI, manuscript as Technical Report 2013-026
  • RALib: A LearnLib extension for inferring EFSMs S. Cassel, F. Howar, B. Jonsson. In DIFTS 15, Int. Workshop on Design and Implementation of Formal Tools and Systems, Austin, Texas USA, September 26-27, 2015. [online proceedings], [author version],
  • Learning Extended Finite State Machines S. Cassel, F. Howar, B. Jonsson, B. Steffen. In SEFM 2014, 12th Int. Conf. on Software Engineering and Formal Methods, LNCS 8702, pp 250-264, Springer 2014. DOI, [author version], extended revised version as Technical Report 2015-032
  • Inferring Semantic Interfaces of Data Structures. F. Howar, M. Isberner, B. Steffen, O. Bauer, B. Jonsson. InProc. ISoLA (1): Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change - 5th Int. Symp.. LNCS 7609: 554-571. Springer, 2012. DOI, [author version],
  • A Succinct Canonical Register Automaton Model for Data Domains with Binary Relations. S. Cassel, B. Jonsson, F. Howar, B. Steffen. In ATVA 2012, Proc. Int. Symp. Automated Technology for Verification and Analysis, LNCS 7561: 57-71. Springer, 2012. DOI, [author version],
  • Demonstrating Learning of Register Automata. M. Merten, F. Howar, B. Steffen, S. Cassel, B. Jonsson. In TACAS 2012: Proc. Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, LNCS 7214: 466-471. Springer, 2012. DOI, [author version],
  • Inferring Canonical Register Automata F. Howar, B. Steffen, B. Jonsson, S. Cassel. In VMCAI 2012 Proc. 13th Int. Conf. on Verification, Model Checking, and Abstract Interpretation. LNCS 7148:251-266, Springer Verlag, 2012. DOI, [author version],
  • Learning of Automata Models Extended with Data Bengt Jonsson in Marco Bernardo, Valérie Issarny (Eds.): Formal Methods for Eternal Networked Software Systems - 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2011. Bertinoro, Italy, June 13-18, 2011. LNCS 6659 pp. 327-349, Springer 2011 DOI, [author version],
  • A Succinct Canonical Register Automaton Model Sofia Cassel, Falk Howar, Bengt Jonsson, Maik Merten, Bernhard Steffen. In ATVA 2011, Proc. Int. Symp. Automated Technology for Verification and Analysis, LNCS 6996: 366-380. Springer, 2011. DOI, [author version], extended version as Technical Report 2013-026
  • Learning of event-recording automata Olga Grinchtein, Bengt Jonsson, Martin Leucker. Theor. Comput. Sci. 411(47): 4029-4054 (2010) DOI, [author version],
  • Generating Models of Infinite-State Communication Protocols Using Regular Inference with Abstraction F. Aarts, B. Jonsson, J. Uijen. In ICTSS 2010, 22nd IFIP WG 6.1 Int. Conf. Testing Software and Systems, Natal, Brazil, LNCS 6435: 188-204, Springer 2010 DOI, [author version], extended version as Technical report ICIS-R13001, Radboud University Nijmegen, January 2013
  • Inferring Compact Models of Communication Protocol Entities T. Bohlin, B. Jonsson, S. Soleimanifard In ISoLA 2010, 4th Int. Symp. on Leveraging Applications of Formal Methods, Verification, and Validation, Part I, Heraklion, Crete, October 18-21, 2010, LNCS 6415: 658-672, Springer 2010 DOI, [author version], On Handling Data in Automata Learning - Considerations from the CONNECT Perspective Falk Howar, Bengt Jonsson, Maik Merten, Bernhard Steffen, Sofia Cassel. In ISoLA 2010, 4th Int. Symp. on Leveraging Applications of Formal Methods, Verification, and Validation, Part II, Heraklion, Crete, October 18-21, 2010. LNCS 6416: 221-235, Springer 2010 DOI, [author version],
  • Regular Inference for State Machines Using Domains with Equality Tests. T. Berg, B. Jonsson, H. Raffelt. In Proc. FASE '08, 11th Int. Conf. on Fundamental Approaches to Software Engineering, LNCS 3961:317-331 (2008). DOI, [(extended) author version],
  • Inference of Event-Recording Automata Using Timed Decision Trees. O. Grinchtein, B. Jonsson, P. Pettersson. In Proc. CONCUR 2006, 15th Int. Conf. on Concurrency Theory, LNCS 4137: 435-449 (2006) DOI, [author version],
  • Regular Inference for State Machines with Parameters. T. Berg, B. Jonsson, H. Raffelt. In Proc. FASE '06, 9th Int. Conf. on Fundamental Approaches to Software Engineering, LNCS 3922: 107-121 (2006).DOI, [author version],
  • Model-Based Testing of Reactive Systems, Advanced Lectures M. Broy, B. Jonsson, J.-P. Katoen, M. Leucker, A. Pretschner (Eds.) LNCS 3472, Springer 2005
  • On the correspondence between conformance testing and regular inference T. Berg, O. Grinchtein, B. Jonsson M. Leucker, M. Leucker, and B. Steffen. In Proc. FASE '05, 8th Int. Conf. on Fundamental Approaches to Software Engineering, LNCS 344: 175-189 (2005). DOI, [author version],
  • Insights to Angluin's learning. T. Berg, B. Jonsson, M. Leucker, and M. Saksena. In Proc. Int. Workshop on Software Verification and Validation (SVV 2003), Electr. Notes Theor. Comput. Sci. 118: 3-18 (2005) DOI, [author version],
  • Learning of event-recording automata. O. Grinchtein, B. Jonsson, and M. Leucker. In FORMATS/FTRTFT, volume 3253 of Lecture Notes in Computer Science, pages 379--396. Springer Verlag, 2004.
  • Specifying and generating test cases using observer automata. J. Blom, A. Hessel, B. Jonsson, and P. Pettersson. In Proc. FATES, 4th. International Workshop on Formal Approaches to Testing of Software, volume 3395 of Lecture Notes in Computer Science, pages 125--139. Springer Verlag, 2004.
  • Generating on-line test oracles from temporal logic specifications. J. Håkansson, B. Jonsson, and O. Lundqvist. Journal of Software Tools for Technology Transfer 4(4):456--471, 2003.
Updated  2016-11-15 09:00:27 by Bengt Jonsson.