Document Open Access Logo

Action Codes

Authors Frits Vaandrager , Thorsten Wißmann

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2023.137.pdf
  • Filesize: 0.94 MB
  • 20 pages

Document Identifiers

Author Details

Frits Vaandrager
  • Radboud University, Nijmegen, The Netherlands
Thorsten Wißmann
  • Radboud University, Nijmegen, The Netherlands
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Funding

  • Vaandrager, Frits: Supported by the NWO TOP project 612.001.852.
  • Wißmann, Thorsten: Supported by the NWO TOP project 612.001.852 (until 2022) and the DFG project 419850228 (since 2023).

Acknowledgements

As part of an MSc thesis project under supervision of the first author, Timo Maarse studied a different and more restricted type of action codes (called action refinements) [T. Maarse, 2020]. It turned out, however, that for these action codes, the concretization operator is not monotone. The present paper arose from our efforts to fix this problem. We thank the anonymous reviewers for their suggestions, Paul Fiterău-Broştean for examples of the use of action codes in model learning, and Jules Jacobs for helpful discussions about Coq. The first author would like to thank Rocco De Nicola for his hospitality at IMT Lucca during the work on this paper.

Cite AsGet BibTex

Frits Vaandrager and Thorsten Wißmann. Action Codes. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 137:1-137:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ICALP.2023.137

Abstract

We provide a new perspective on the problem how high-level state machine models with abstract actions can be related to low-level models in which these actions are refined by sequences of concrete actions. We describe the connection between high-level and low-level actions using action codes, a variation of the prefix codes known from coding theory. For each action code ℛ, we introduce a contraction operator α_ℛ that turns a low-level model ℳ into a high-level model, and a refinement operator ϱ_ℛ that transforms a high-level model 𝒩 into a low-level model. We establish a Galois connection ϱ_ℛ(𝒩) ⊑ ℳ ⇔ 𝒩 ⊑ α_ℛ(ℳ), where ⊑ is the well-known simulation preorder. For conformance, we typically want to obtain an overapproximation of model ℳ. To this end, we also introduce a concretization operator γ_ℛ, which behaves like the refinement operator but adds arbitrary behavior at intermediate points, giving us a second Galois connection α_ℛ(ℳ) ⊑ 𝒩 ⇔ ℳ ⊑ γ_ℛ(𝒩). Action codes may be used to construct adaptors that translate between concrete and abstract actions during learning and testing of Mealy machines. If Mealy machine ℳ models a black-box system then α_ℛ(ℳ) describes the behavior that can be observed by a learner/tester that interacts with this system via an adaptor derived from code ℛ. Whenever α_ℛ(ℳ) implements (or conforms to) 𝒩, we may conclude that ℳ implements (or conforms to) γ_ℛ (𝒩). Almost all results, examples, and counter-examples are formalized in Coq.

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • Automata
  • Models of Reactive Systems
  • LTS
  • Action Codes
  • Action Refinement
  • Action Contraction
  • Galois Connection
  • Model-Based Testing
  • Model Learning

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. F. Aarts, B. Jonsson, J. Uijen, and F.W. Vaandrager. Generating models of infinite-state communication protocols using regular inference with abstraction. Formal Methods in System Design, 46(1):1-41, 2015. URL: https://doi.org/10.1007/s10703-014-0216-x.
  2. M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 1(15):73-132, 1993. Google Scholar
  3. G. Behrmann, A. David, K. G. Larsen, J. Håkansson, P. Pettersson, W. Yi, and M. Hendriks. Uppaal 4.0. In Third International Conference on the Quantitative Evaluation of SysTems (QEST 2006), 11-14 September 2006, Riverside, CA, USA, pages 125-126. IEEE Computer Society, 2006. Google Scholar
  4. J.A. Bergstra, A. Ponse, and S.A. Smolka, editors. Handbook of Process Algebra. North-Holland, 2001. Google Scholar
  5. J. Berstel and D. Perrin. Theory of codes. Academic Press, 1985. Google Scholar
  6. M. van der Bijl, A. Rensink, and J. Tretmans. Compositional testing with ioco. In A. Petrenko and A. Ulrich, editors, Formal Approaches to Software Testing, Third International Workshop on Formal Approaches to Testing of Software, FATES 2003, Montreal, Quebec, Canada, October 6th, 2003, volume 2931 of Lecture Notes in Computer Science, pages 86-100. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24617-6_7.
  7. M. van der Bijl, A. Rensink, and J. Tretmans. Action refinement in conformance testing. In F. Khendek and R. Dssouli, editors, Testing of Communicating Systems, 17th IFIP TC6/WG 6.1 International Conference, TestCom 2005, Montreal, Canada, May 31 - June 2, 2005, Proceedings, volume 3502 of Lecture Notes in Computer Science, pages 81-96. Springer, 2005. Google Scholar
  8. J. Burton, M. Koutny, and G. Pappalardo. Implementing communicating processes in the event of interface difference. In 2nd International Conference on Application of Concurrency to System Design (ACSD 2001), 25-30 June 2001, Newcastle upon Tyne, UK, page 87. IEEE Computer Society, 2001. URL: https://doi.org/10.1109/CSD.2001.981767.
  9. G. Chalupar, S. Peherstorfer, E. Poll, and J. de Ruiter. Automated reverse engineering using Lego. In Proceedings 8th USENIX Workshop on Offensive Technologies (WOOT'14), San Diego, California, Los Alamitos, CA, USA, August 2014. IEEE Computer Society. Google Scholar
  10. E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, Cambridge, Massachusetts, 1999. Google Scholar
  11. P. Fiterău-Broştean, R. Janssen, and F.W. Vaandrager. Combining model learning and model checking to analyze TCP implementations. In S. Chaudhuri and A. Farzan, editors, Proceedings 28th International Conference on Computer Aided Verification (CAV'16), Toronto, Ontario, Canada, volume 9780 of Lecture Notes in Computer Science, pages 454-471. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41540-6_25.
  12. P. Fiterău-Broştean, B. Jonsson, R. Merget, J. de Ruiter, K. Sagonas, and J. Somorovsky. Analysis of DTLS implementations using protocol state fuzzing. In 29th USENIX Security Symposium (USENIX Security 20), pages 2523-2540. USENIX Association, August 2020. Google Scholar
  13. P. Fiterău-Broştean, T. Lenaerts, E. Poll, J. de Ruiter, F. Vaandrager, and P. Verleg. Model learning and model checking of SSH implementations. In Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, SPIN 2017, pages 142-151, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3092282.3092289.
  14. H. Garavel and F. Lang. Equivalence checking 40 years after: A review of bisimulation tools. In N. Jansen, M. Stoelinga, and P. van den Bos, editors, A Journey from Process Algebra via Timed Automata to Model Learning, pages 213-265, Cham, 2022. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-15629-8_13.
  15. R.J. van Glabbeek. The linear time - Branching time spectrum I. The semantics of concrete, sequential processes. In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, pages 3-99. North-Holland, 2001. Google Scholar
  16. R.J. van Glabbeek and U. Goltz. Equivalence notions for concurrent systems and refinement of actions (extended abstract). In A. Kreczmar and G. Mirkowska, editors, Mathematical Foundations of Computer Science 1989, MFCS'89, Porabka-Kozubnik, Poland, August 28 - September 1, 1989, Proceedings, volume 379 of Lecture Notes in Computer Science, pages 237-248. Springer, 1989. URL: https://doi.org/10.1007/3-540-51486-4_71.
  17. R.J. van Glabbeek and U. Goltz. Refinement of actions and equivalence notions for concurrent systems. Acta Informatica, 37(4/5):229-327, 2001. URL: https://doi.org/10.1007/s002360000041.
  18. R. Gorrieri and A. Rensink. Action refinement. In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, pages 1047-1147. North-Holland, 2001. Google Scholar
  19. J.F. Groote and F.W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100(2):202-260, October 1992. Google Scholar
  20. C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, 1985. Google Scholar
  21. J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979. Google Scholar
  22. R. Janssen, F.W. Vaandrager, and J. Tretmans. Relating alternating relations for conformance and refinement. In W. Ahrendt and S. Lizeth Tapia Tarifa, editors, Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings, volume 11918 of Lecture Notes in Computer Science, pages 246-264. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-34968-4_14.
  23. M. Koutny and G. Pappalardo. The ERT model of fault-tolerant computing and its application to a formalisation of coordinated atomic actions. Report 636, Department of Computing Science, University of Newcastle upon Tyne, 1998. URL: http://www.cs.ncl.ac.uk/publications/trs/papers/636.pdf.
  24. L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872-923, May 1994. Google Scholar
  25. D. Lee and M. Yannakakis. Principles and methods of testing finite state machines - a survey. Proceedings of the IEEE, 84(8):1090-1123, 1996. Google Scholar
  26. N.A. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, Inc., San Fransisco, California, 1996. Google Scholar
  27. N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6^th Annual ACM Symposium on Principles of Distributed Computing, pages 137-151, August 1987. A full version is available as MIT Technical Report MIT/LCS/TR-387. Google Scholar
  28. N.A. Lynch and F.W. Vaandrager. Forward and backward simulations, I: Untimed systems. Information and Computation, 121(2):214-233, September 1995. Google Scholar
  29. T. Maarse. Active Mealy Machine Learning Using Action Refinements. Master’s thesis, Radboud University, Institute for Computing and Information Sciences, August 2020. Google Scholar
  30. R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989. Google Scholar
  31. A. Rensink and R. Gorrieri. Vertical implementation. Information and Computation, 170(1):95-133, 2001. URL: https://doi.org/10.1006/inco.2001.2967.
  32. J. de Ruiter and E. Poll. Protocol state fuzzing of TLS implementations. In 24th USENIX Security Symposium, pages 193-206, Washington, D.C., August 2015. USENIX Association. URL: https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/de-ruiter.
  33. C. McMahon Stone, T. Chothia, and J. de Ruiter. Extending automated protocol state learning for the 802.11 4-way handshake. In J. López, J. Zhou, and M. Soriano, editors, Computer Security - 23rd European Symposium on Research in Computer Security, ESORICS 2018, Barcelona, Spain, September 3-7, 2018, Proceedings, Part I, volume 11098 of Lecture Notes in Computer Science, pages 325-345. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-99073-6_16.
  34. A.S. Tanenbaum and D. Wetherall. Computer networks, 5th Edition. Pearson, 2011. URL: https://www.worldcat.org/oclc/698581231.
  35. J. Tretmans. Test generation with inputs, outputs, and repetitive quiescence. Software-Concepts and Tools, 17:103-120, 1996. Google Scholar
  36. J. Tretmans. Model based testing with labelled transition systems. In R.M. Hierons, J.P. Bowen, and M. Harman, editors, Formal Methods and Testing, An Outcome of the FORTEST Network, Revised Selected Papers, volume 4949 of Lecture Notes in Computer Science, pages 1-38. Springer, 2008. Google Scholar
  37. F.W. Vaandrager. Model learning. Communications of the ACM, 60(2):86-95, February 2017. URL: https://doi.org/10.1145/2967606.
  38. F.W. Vaandrager, B. Garhewal, J. Rot, and T. Wißmann. A new approach for active automata learning based on apartness. In D. Fisman and G. Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243 of Lecture Notes in Computer Science, pages 223-243. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_12.
  39. P. Verleg. Inferring SSH state machines using protocol state fuzzing. Master thesis, Radboud University Nijmegen, February 2016. URL: https://www.ru.nl/publish/pages/769526/z07_patrick_verleg.pdf.
  40. M. Yannakakis. Hierarchical state machines. In J. van Leeuwen, O. Watanabe, M. Hagiya, P.D. Mosses, and T. Ito, editors, Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics, pages 315-330, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact