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

DOI10.1007/S10703-014-0216-XzbMATH Open1322.68131OpenAlexW2561427878MaRDI QIDQ2018056FDOQ2018056

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

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

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)

Cites Work

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

Cited In (8)

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

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)