Nach Typ filtern:

Nach Jahr sortieren:

SMA—The Smyle Modeling Approach

Carsten Kern, Benedikt Bollig, Joost-Pieter Katoen, Martin Leucker
Conference Papers Proceedings 3rd IFIP TC2 Central and East European Conference on Software Engineering Techniques (CEE-SET 2008), Volume 4980 of LNCS, pages 103–117

Keywords: Software Engineering, Design Models, Automatic Model Generation, Model Inference, Testing, Model Driven Testing, Automatic Testgeneration

Abstract

This paper introduces the model-based software development methodology SMA—the Smyle Modeling Approach—which is centered around Smyle, a dedicated learning procedure to support engineers to interactively obtain design models from requirements, characterized as either being desired (positive) or unwanted (negative) system behavior. The learning approach is complemented by scenario patterns where the engineer can specify clearly desired or unwanted behavior. This way, user interaction is reduced to the interesting scenarios limiting the design effort considerably. In SMA, the learning phase is complemented by an effective analysis phase that allows for detecting design flaws at an early design stage. This paper describes the approach and reports on first practical experiences.

Learning Communicating Automata from MSCs

Carsten Kern, Benedikt Bollig, Joost-Pieter Katoen, Martin Leucker
Journal Paper IEEE Transactions on Software Engineering, Volume 36, pages 390–408

Keywords: Requirements, Sequence Diagrams, Distributed Systems, Communicating Automata, Model Inference, Learning Algorithms, Artificial Intelligence

Abstract

This paper is concerned with bridging the gap between requirements and distributed systems. Requirements are defined as basic message sequence charts (MSCs) specifying positive and negative scenarios. Communicating finite-state machines (CFMs), i.e., finite automata that communicate via FIFO buffers, act as system realizations. The key contribution is a generalization of Angluin's learning algorithm for synthesizing CFMs from MSCs. This approach is exact-the resulting CFM precisely accepts the set of positive scenarios and rejects all negative ones-and yields fully asynchronous implementations. The paper investigates for which classes of MSC languages CFMs can be learned, presents an optimization technique for learning partial orders, and provides substantial empirical evidence indicating the practical feasibility of the approach.

SMA: The Smyle Modeling Approach

Carsten Kern, Benedikt Bollig, Joost-Pieter Katoen, Martin Leucker
Journal Paper Computing and Informatics, Volume 29, pages 45–72

Keywords: Software Engineering, Design Models, Automatic Model Generation, Model Inference, Testing, Model Driven Testing, Automatic Testgeneration

Abstract

This paper introduces the model-based software development lifecycle model SMA – the Smyle Modeling Approach – which is centered around Smyle. Smyle is a dedicated learning procedure to support engineers to interactively obtain design models from requirements, characterized as either being desired (positive) or unwanted (negative) system behavior. Within SMA, the learning approach is complemented by so-called scenario patterns where the engineer can specify clearlydesired or unwanted behavior. This way, user interaction is reduced to the interesting scenarios limiting the design effort considerably. In SMA, the learning phase is further complemented by an effective analysis phase that allows for detecting design flaws at an early design stage. Using learning techniques allows us to gradually develop and refine requirements, naturally supporting evolving requirements, and allows for a rather inexpensive redesign in case anomalous system behavior is detected during analysis, testing, or maintenance. This paper describes the approach and reports on first practical experiences.

libalf: the Automata Learning Framework

Carsten Kern, Benedikt Bollig, Joost-Pieter Katoen, Martin Leucker, Daniel Neider, David Piegdon
Conference Papers Computer-Aided Verification (CAV), Volume 6174 of LNCS, pages 360–364, Springer Verlag

Keywords: Automata Learning, Model Inference, Learning Library, Artificial Intelligence, Machine Learning, Verification, Model Checking

Abstract

This paper presents libalf, a comprehensive, open-source library for learning formal languages. libalf covers various well-known learning techniques for finite automata (e.g. Angluin’s L* , Biermann, RPNI etc.) as well as novel learning algorithms (such as for NFA and visibly one-counter automata). libalf is flexible and allows facilely interchanging learning algorithms and combining domain-specific features in a plug-and-play fashion. Its modular design and C++ implementation make it a suitable platform for adding and engineering further learning algorithms for new target models (e.g., Buechi automata).

Learning Communicating and Nondeterministic Automata

Carsten Kern
Theses Ph.D. Thesis at RWTH Aachen University

Keywords: Software Engineering, Verification, Model Checking, PDL, Partial Order Reduction, Automatic Model Generation, Model Inference, Testing, Model Driven Testing, Automatic Testgeneration

Abstract

The results of this dissertation are two-fold. On the one hand, inductive learning techniques are extended and two new inference algorithms for inferring nondeterministic, and universal, respectively, finite-state automata are presented. On the other hand, certain learning techniques are employed and enhanced to semi-automatically infer communicating automata (also called design models in the software development cycle). For both topics, theoretical results on the feasibility of the approaches, as well as an implementation are presented which, in both cases, support our theory. Concerning the first objective to derive a so-called active online learning algorithm for nondeterministic finite-state automata (NFA), we present, in analogy to Angluin's famous learning algorithm L* for deterministic finite-state automata (DFA), a version for inferring a certain subclass of NFA. The automata from this class are called residual finite-state automata (RFSA). It was shown by Denis et al. that there is an exponential gap between the size of minimal DFA and their corresponding minimal RFSA. Even if there are also cases where the canonical (i.e., minimal) RFSA is exponentially larger than a corresponding minimal NFA, we show that the new learning algorithm---called NL*---is a great improvement compared to L* as the inferred canonical RFSA has always at most the size of the corresponding minimal DFA but is usually even considerably smaller and more easy to learn. Unlike a learning procedure developed by Denis et al.---called DeLeTe2---our algorithm is capable of deriving canonical RFSA. Like L*, the new algorithm will be applicable in many fields including pattern recognition, computational linguistics and biology, speech recognition, and verification. From our point of view, NL* might especially play a mayor role in the area of formal verification where the size of the models that are processed is of enormous importance and nondeterminism not regarded an unpleasant property. The second objective of this thesis is to create a method for inferring distributed design models (CFMs) from a given set of requirements specified as scenarios (message sequence charts). The main idea is to extend the L* algorithm to cope with valid and invalid sets of system runs and, after some iterations, come up with an intermediate design model (a DFA) which exhibits features that make it distributable into communicating components (or processes) interacting via FIFO channels. Theoretical results on which classes of CFMs are learnable in which time-complexity bounds are presented. We also developed a tool implementation called Smyle, realizing important theoretical results evolving from this part of the thesis. Based on this learning formalism we also derive a software-engineering lifecycle model called the Smyle Modeling Approach in which we embedded our learning approach. Additionally, we launched a project for a new learning library called libalf which includes most of the learning algorithms (and their extensions) mentioned in this thesis. We hope that, due to its continuously increasing functionality, libalf will find broad acceptance among researchers, and that it will be the starting point for an extensive project of different research groups which will employ libalf, or augment the library with new algorithms.

Angluin-style learning of NFA

Carsten Kern, Benedikt Bollig, Peter Habermehl, Martin Leucker
Conference Papers Proceedings of the Twenty-first International Joint Conference on Artificial Intelligence (IJCAI-09), pages 1004–1009, AAAI Press

Keywords: Model Inference, Learning Algorithms, Artificial Intelligence, Nondeterministic Automata

Abstract

We introduce NL*, a learning algorithm for inferring non-deterministic finite-state automata usingmembership and equivalence queries. More specifically, residual finite-state automata (RFSA) are learned similarly as in Angluin’s popular L* algorithm, which, however, learns deterministic finite-state automata (DFA). Like in a DFA, the states of an RFSA represent residual languages. Unlike a DFA, an RFSA restricts to prime residual languages, which cannot be described as the union of other residual languages. In doing so, RFSA can be exponentially more succinct than DFA. They are, therefore, the preferable choice for many learning applications. The implementation of our algorithm is applied to a collection of examples and confirms the expected advantage of NL* over L*.

Angluin-Style Learning of NFA

Carsten Kern, Benedikt Bollig, Peter Habermehl, Martin Leucker
Technical Report Technical report at Laboratoire Spécification et Vérification, ENS Cachan, France number LSV-08-28

Keywords: Model Inference, Learning Algorithms, Artificial Intelligence, Nondeterministic Automata

Abstract

This paper introduces NL*, a learning algorithm for inferring non-deterministic finite-state automata using membership and equivalence queries. More specifically, residual finite-state automata (RFSA) are learned similar as in Angluin’s popular L* algorithm, which however learns deterministic finite-state automata (DFA). As RFSA can be exponentially more succinct than DFA, RFSA are the preferable choice for many learning applications. The implementation of our algorithms is applied to a collection of examples and confirms the expected advantage of NL* over L*.

Smyle: a Tool for Synthesizing Distributed Models from Scenarios by Learning

Carsten Kern, Benedikt Bollig, Joost-Pieter Katoen, Martin Leucker
Conference Paper 19th International Conference on Concurrency Theory (CONCUR'08), Volume 5201 of LNCS, pages 162–166

Keywords: Tool, Distributed Systems, Requirements, Automatic Design Model Generation, Automatic Testcase Generation, Learning Algorithms

Abstract

This paper presents Smyle, a tool for synthesizing asynchronous and distributed implementation models from sets of scenarios that are given as message sequence charts (MSCs). The latter specify desired or unwanted behavior of the system to be. Provided with such positive and negative example scenarios, Smyle employs dedicated learning techniques and propositional dynamic logic (PDL) over MSCs to generate a system model that conforms with the given examples.

Replaying Play in and Play out: Synthesis of Design Models from Scenarios by Learning

Carsten Kern, Benedikt Bollig, Joost-Pieter Katoen, Martin Leucker
Conference Paper Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'07), Volume 4424 of LNCS, pages 435–450, Springer Verlag

Keywords: Software Engineering, Distributed Systems, Requirements, Automatic Design Model Generation, Automatic Testcase Generation, Learning Algorithms

Abstract

This paper is concerned with bridging the gap between requirements, provided as a set of scenarios, and conforming design models. The novel aspect of our approach is to exploit learning for the synthesis of design models. In particular, we present a procedure that infers a message-passing automaton (MPA) from a given set of positive and negative scenarios of the system’s behavior provided as message sequence charts (MSCs). The paper investigates which classes of regular MSC languages and corresponding MPA can (not) be learned, and presents a dedicated tool based on the learning library LearnLib that supports our approach.

Replaying Play in and Play out: Synthesis of Design Models from Scenarios by Learning

Carsten Kern, Benedikt Bollig, Joost-Pieter Katoen, Martin Leucker
Technical Report Technical report at RWTH Aachen number AIB-2006-12

Keywords: Software Engineering, Distributed Systems, Requirements, Automatic Design Model Generation, Automatic Testcase Generation, Learning Algorithms

Abstract

This paper is concerned with bridging the gap between requirements, provided as a set of scenarios, and conforming design models. The novel aspect of our approach is to exploit learning for the synthesis of design models. In particular, we present a procedure that infers a message-passing automaton (MPA) from a given set of positive and negative scenarios of the system’s behavior provided as message sequence charts (MSCs). The paper investigates which classes of regular MSC languages and corresponding MPAs can (not) be learned, and presents a dedicated tool based on the learning library LearnLib that supports our approach.

MSCan - A Tool for Analyzing MSC Specifications

Carsten Kern, Benedikt Bollig, Markus Schlütter, Volker Stolz
Conference Papers Proceedings of the 12th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'06), Volume 3920 of LNCS, pages 455–458, Springer

Keywords: Tool, Software Engineering, Distributed Systems, Requirements, Verification, Model Checking, Static Analysis, Analysis of Properties of Distributed Systems

Abstract

We present the tool MSCan, which supports MSC-based system development. In particular, it automatically checks high-level MSC specifications for implementability.

MSCan - Ein Tool zur Analyse von Message Sequence Charts

Carsten Kern
Theses Diploma Thesis at Faculty of Mathematics, Computer Sciences and Natural Sciences, RWTH Aachen University

Keywords: Software Engineering, Distributed Systems, Requirements, Verification, Model Checking, Static Analysis, Analysis of Properties of Distributed Systems