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.
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.
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.
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).
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.
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*.
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*.
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.
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.
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.
We present the tool MSCan, which supports MSC-based system development. In particular, it automatically checks high-level MSC specifications for implementability.