Generating models of infinite-state communication protocols using regular inference with abstraction

DOI10.1007/S10703-014-0216-XMaRDI QIDQ2018056zbMATH OpenOpenAlexFDO

Authors Fides Aarts, Bengt Jonsson, Johan Uijen, F. Vaandrager

Publication date 24 March 2015

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-014-0216-x

zbMATH Keywords

communication protocolsabstraction techniquesactive automata learningMealy machinessession initiation protocoltransmission control protocol

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Network protocols (68M12)

Recommendations

• Regular model checking using inference of regular languages
• Abstraction and learning for infinite-state compositional verification
• Fundamental Approaches to Software Engineering
• Computer Aided Verification
• scientific article; zbMATH DE number 2087513

Cites work

• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 571346 (Why is no real title available?)
• scientific article; zbMATH DE number 1956591 (Why is no real title available?)
• scientific article; zbMATH DE number 2080060 (Why is no real title available?)
• scientific article; zbMATH DE number 2087513 (Why is no real title available?)
• scientific article; zbMATH DE number 1418458 (Why is no real title available?)
• 25 years of model checking. History, achievements, perspectives
• A Succinct Canonical Register Automaton Model
• A theory of history dependent abstractions for learning interface automata
• Automata Learning through Counterexample Guided Abstraction Refinement
• Automata learning with automated alphabet abstraction refinement
• Counterexample-guided abstraction refinement for symbolic model checking
• Demonstrating Learning of Register Automata
• Domain-specific optimization in automata learning.
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Generating models of infinite-state communication protocols using regular inference with abstraction
• Handbook of process algebra
• Improving active Mealy machine learning for protocol conformance testing
• Inference of finite automata using homing sequences
• Integration Testing of Distributed Components Based on Learning Parameterized I/O Models
• Language identification in the limit
• Lazy abstraction
• Learning regular sets from queries and counterexamples
• Mining specifications
• Model-based testing of reactive systems. Advanced lectures.
• Network invariants for real-time systems
• Property preserving abstractions for the verification of concurrent systems
• Symbolic finite state transducers: algorithms and applications

Cited in

(8)

• Fingerprinting and analysis of Bluetooth devices with automata learning
• Active learning for extended finite state machines
• A Myhill-Nerode theorem for register automata and symbolic trace languages
• Learning realtime one-counter automata
• Generating models of infinite-state communication protocols using regular inference with abstraction
• A novel learning algorithm for Büchi automata based on family of DFAs and classification trees
• scientific article; zbMATH DE number 2087513 (Why is no real title available?)
• History-preserving bisimilarity for higher-dimensional automata via open maps

Describes a project that uses

Uses Software

• SLAM
• LearnLib
• SpecExplorer
• ns-2

This page was built for publication: Generating models of infinite-state communication protocols using regular inference with abstraction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2018056)