Search

Inferring behavioral models (e.g., state machines) of software systems is an important element of re-engineering activities. Model inference techniques can be categorized as active or passive learning, constructing models by (dynamically) interacting with systems or (statically) analyzing traces, respectively. Application of those techniques in the industry is, however, hindered by the trade-off between learning time and completeness achieved (active learning) or by incomplete input logs (passive learning). We investigate the learning time/completeness achieved trade-off of active learning with a pilot study at ASML, provider of lithography systems for the semiconductor industry. To resolve the trade-off we advocate extending active learning with execution logs and passive learning results.We apply the extended approach to eighteen components used in ASML TWINSCAN lithography machines. Compared to traditional active learning, our approach significantly reduces the active learning time. Moreover, it is capable of learning the behavior missed by the traditional active learning approach.

Model-based languages such as MATLAB/Simulink play an essential role in the model-driven development of software systems. To comply with new requirements, it is common practice to create new variants by copying existing systems and modifying them. Commonly referred to as clone-and-own, severe problems arise in the long-run when no dedicated variability management is installed. To allow for a documented and structured reuse of systems, their variability information needs to be reverse-engineered. In this paper, we propose an advanced comparison procedure, the Matching Window Technique, and a customizable metric. Both allow us to overcome structural alterations commonly performed during clone-and-own. We analyze related MATLAB/Simulink models and determine, classify and represent their variability information in an understandable way. With our technique, we assist model engineers in maintaining and evolving existing variants. We provide three feasibility studies with real-world models from the automotive domain and show our technique to be fast and precise. Furthermore, we perform semi-structured interviews with domain experts to assess the potential applicability of our technique in practice.

Minimal acyclic deterministic finite automata (MADFAs) are used to represent dictionaries, i.e., finite sets of finite words, in, e.g., spell checkers and network security applications. Given the size of such dictionaries, which may contain millions of words, their efficient construction is a critical issue. Watson (2010) published a classification of such algorithms in an algorithm taxonomy with correctness arguments. We report on a new algorithm which constructs MADFAs in parallel---each for a keyword set from a partition of the original keyword set---and afterwards merges and minimizes the resulting automata into a single MADFA; on our experience implementing the algorithms in a Java-based toolkit; and on empirical performance results obtained.

We present a minimization algorithm for finite state automata that finds and merges bisimulation-equivalent states, identified through partition aggregation. We show the algorithm to be correct and run in time \( O \left( n^2 d^2 \left| \Sigma \right| \right) \), where n is the number of states of the input automaton \(M\), d is the maximal outdegree in the transition graph for any combination of state and input symbol, and \(\left| \Sigma \right| \) is the size of the input alphabet. The algorithm is slower than those based on partition refinement, but has the advantage that intermediate solutions are also language equivalent to \(M\). As a result, the algorithm can be interrupted or put on hold as needed, and the derived automaton is still useful. Furthermore, the algorithm essentially searches for the maximal model of a characteristic formula for \(M\), so many of the optimisation techniques used to gain efficiency in SAT solvers are likely to apply.

Correctness-by-construction (CbC), traditionally based on weakest precondition semantics, and post-hoc verification (PhV) aspire to ensure functional correctness. We argue for a lightweight approach to CbC where lack of formal rigour increases productivity. In order to mitigate the risk of accidentally introducing errors during program construction, we propose to complement lightweight CbC with PhV. We introduce lightweight CbC by example and discuss strength and weaknesses of CbC and PhV and their combination, both conceptually and using a case study.

Modern software systems, in particular in mobile and cloud-based applications, exist in many different variants in order to adapt to changing user requirements or application contexts. Software product line engineering allows developing these software systems by managed large-scale reuse in order to achieve shorter time to market. Traditional software product line engineering approaches use a domain variability model which only captures the configuration options of the product variants, but does not provide any guideline for designing and implementing reusable artifacts. In contrast, software taxonomies structure software domains from an abstract specification of the functionality to concrete implementable variants by successive correctness-preserving refinements. In this paper, we propose a novel software product line engineering process based on a taxonomy-based domain analysis. The taxonomy’s hierarchy provides guidelines for designing and implementing the product line’s reusable artifacts while at the same time specifying possible configuration options. By deriving reusable product line artifacts from a software taxonomy, the well-defined structuring of the reusable artifacts yields improved maintainability and evolvability of the product line.

Many applications in Model-Driven Engineering involve processing multiple models or metamodels. A good example is the comparison and merging of metamodel variants into a common metamodel in domain model recovery. Although there are many sophisticated techniques to process the input dataset, little attention has been given to the initial data analysis, visualization and filtering activities. These are hard to ignore especially in the case of a large dataset, possibly with outliers and sub-groupings. In this paper we present a generic approach for metamodel comparison, analysis and visualization as an exploratory first step for domain model recovery. We propose representing metamodels in a vector space model, and applying hierarchical clustering techniques to compare and visualize them as a tree structure. We demonstrate our approach on two Ecore datasets: a collection of 50 state machine metamodels extracted from GitHub as top search results; and ∼ ∼100 metamodels from 16 different domains, obtained from AtlanMod Metamodel Zoo.

Inspired by failure functions found in classical pattern matching algorithms, a failure deterministic finite automaton (FDFA) is defined as a formalism to recognise a regular language. An algorithm, based on formal concept analysis, is proposed for deriving from a given deterministic finite automaton (DFA) a language-equivalent FDFA. The FDFA’s transition diagram has fewer arcs than that of the DFA. A small modification to the classical DFA’s algorithm for recognising language elements yields a corresponding algorithm for an FDFA.

We present an approach to model hardware configurations of complex manufacturing systems such as ASML's lithography machines. These hardware configurations consist of actuator and sensor elements which are controlled by system software that consists of over 35 million lines of code. To minimize the cost of testing and system integration, software simulators of hardware configurations are used - acting as virtual hardware platforms on which the real control software can be executed and tested. An important aspect in such simulation and testing is material flow (specifically wafer flow) in the machine. To support the effective and efficient realization of simulators covering material flow, we defined a domain specific language (DSL) for modelling the hardware configurations to be simulated, and used a model-driven engineering approach to generate the software components implementing the simulators. The DSL can be used to specify not only nominal (i.e. good weather) behaviour but also simulation based fault injection scenarios. The overall approach reduces the cost of early hardware-software integration and enables simulating scenarios that cannot be executed on real machines because they are difficult or hazardous to carry out.

In recent years, the range of alphabet sizes typically used in applications of finite automata has grown considerably, now ranging from DNA alphabets—whose symbols are representable using 2 bits—to Unicode alphabets—whose symbol representation may take up to 32 bits. As automata traditionally use symbol encodings taking 8 bits, the different alphabet and symbol sizes bring up the question whether they may be exploited to either decrease memory use for the automata’s transition tables or to decrease string processing time. In [3], stretching and jamming were introduced as transformations on finite automata. Given a finite automaton, we can stretch it by splitting each single transition into two or more sequential transitions, thereby introducing additional intermediate states. Jamming is the inverse transformation, in which two or more successive transitions are joined into a single transition, thereby removing redundant intermediate states. In this paper, we only consider a restricted form of stretching and jamming, in which a fixed factor is used to stretch (jam) transitions (transition paths) in a given automaton, and in which transition symbols are assumed to be encoded as bit strings. We consider improved versions of the algorithms that were presented in [3] for this particular form of stretching and jamming. The algorithms were implemented in c++ and used to benchmark the transformations. The results of this benchmarking indicate that, under certain conditions, stretching may be beneficial to memory use to the detriment of processing time, while jamming may be beneficial to processing time to the detriment of memory use. The latter seems potentially useful in the case of DNA processing, while the former may be for Unicode processing. Keywords: finite automata; transformation; split transition; join transition; transition table size; string processing time

We report on a toolkit of tree automata and algorithms for tree acceptance, pattern matching, and parsing. Despite many applications, no large toolkit of such algorithms existed, complicating choice among them. Our toolkit's design was guided by our taxonomies of such algorithms, and this is clearly reflected in its structure. We outline one taxonomy and discuss how its hierarchy determines the toolkit's class and interface hierarchies. The toolkit, available at http://www.fastar.org , contains about 50 tree algorithms and automata constructions.

Algorithms for acceptance, pattern matching and parsing of regular trees and the tree automata used in these algorithms have many applications, including instruction selection in compilers, implementation of term rewriting systems, and model checking. Many such tree algorithms and constructions for such tree automata appear in the literature, but some deficiencies existed, including: inaccessibility of theory and algorithms; difficulty of comparing algorithms due to variations in presentation style and level of formality; and lack of reference to the theory in many publications. An algorithm taxonomy is an effective means of bringing order to such a field. We report on two taxonomies of regular tree algorithms that we have constructed to deal with the deficiencies. The complete work has been presented in the PhD thesis of the first author.

The subject of this dissertation is the construction of two taxonomies and a toolkit of algorithms solving two different but closely related problems from the domain of regular tree languages. In our context, a taxonomy is a classification of algorithms according to their essential details. Its starting point is a high-level algorithm whose correctness is easily shown. By adding details, one obtains refinements or variations of that algorithm and of algorithms obtained in such a way. This may lead to algorithms from the literature or to new ones. Every detail has correctness arguments associated with it, so that each algorithm’s correctness follows from the correctness of the starting point and details added. The sequence of details from the starting point to an algorithm shows how the algorithm can be obtained from the starting point and can be used to characterize the particular algorithm. An algorithm taxonomy may be depicted as a directed acyclic graph, in which nodes refer to algorithms and branches refer to details. We construct taxonomies for two algorithmic problems from the domain of regular tree languages on ordered, ranked trees. This domain has a rich theory, and parts of this theory have broad applicability in areas such as code generation in compilers—particularly for instruction selection or optimization—and term rewriting. Underlying the practical applications are a number of algorithmic problems, of which tree acceptance and tree pattern matching are two. Many algorithms solving these problems have been described and used in practice. Unfortunately, the domain suffers from a number of deficiencies: 1. Inaccessibility of the theory and algorithms, as they are scattered over the literature and few or no overview publications—particularly algorithm oriented ones—exist. 2. Difficulty of comparing the algorithms due to differences in presentation style and level of formality. 3. Lack of reference to the theory and of correctness arguments in publications of practical algorithms. 4. Lack of a large and coherent collection of implementations of the algorithms. 5. Difficulty of choosing between different algorithms for practical applications. The construction of taxonomies aims to solve the first three deficiencies. The construction process is part of TABASCO, a method for domain modeling and domain engineering for a particular kind of domain in computer science. As a first step, an overview of relevant parts of the theory is created. A literature survey is then performed to gather algorithms solving the algorithmic problem or problems. Based on the results, the algorithms are rephrased in a common presentation style and a model in the form of an algorithm taxonomy for the algorithmic problem or problems is constructed. The taxonomy makes the commonalities and variations between the algorithms as well as the correctness arguments for the algorithms explicit. The problems of tree acceptance and tree pattern matching are related and the algorithms solving them involve many of the same algorithmic ingredients. The commonalities lead to similarities between the taxonomies constructed for each of the two problems. Furthermore, references to and discussions of the algorithms’ occurrences in the literature are included. The last two of the five deficiencies mentioned above can be solved using TABASCO’s domain engineering steps, which include the creation of a toolkit of algorithm implementations and of a domain specific language to allow more effective use of such a toolkit. The design of a coherent toolkit is simplified by the availability of a taxonomy, which indicates the commonalities and differences between the various algorithms. The high-level design choices are guided by the taxonomy structure, and the choice of which language constructs to use to implement various design parts can be made based on standard design techniques. We consider the domain of keyword pattern matching as a brief case study for all of the method’s domain engineering steps. For the domain of regular tree languages, we consider the design of a toolkit of tree acceptance and tree pattern matching algorithms based on the two taxonomies. The taxonomy-based toolkit design results in a coherent and easily extendable toolkit.

The keyword pattern matching problem has been frequently studied, and many different algorithms for solving it have been suggested. Watson and Zwaan in the early 1990s derived a set of well-known solutions from a common starting point, leading to a taxonomy of such algorithms. Their taxonomy allowed one to easily compare the different algorithms, and to easily implement them in a taxonomy-based toolkit. The taxonomy and toolkit did not include a variant of the Boyer-Moore algorithm developed by Horspool. In this paper, we present the Boyer-Moore-Horspool algorithm and its multiple keyword generalization in the context of the taxonomy.

In this paper, we present data structures and algorithms for efficiently constructing approximate automata. An approximate automaton for a regular language L is one which accepts at least L. Such automata can be used in a variety of practical applications, including network security pattern matching, in which false-matches are only a performance nuisance. The construction algorithm is particularly efficient, and is tunable to yield more or less exact automata.

Derivatives of regular expressions were first introduced by Brzozowski in [1]. By recursively computing all derivatives of a regular expression, and associating a state with each unique derivative, a deterministic finite automaton can be constructed. Convergence of this process is guaranteed if uniqueness of regular expressions is recognized modulo associativity, commutativity, and idempotence of the union operator. Additionaly, through simplification based on the identities for regular expressions, the number of derivatives can be further reduced.

We discuss a new tool, FIRE Station, for the visualization, exploration and manipulation of regular languages and their various representations, including regular expressions and finite state automata.

In this paper we present two transformations on automata, called stretching and jamming. These transformations will, under certain conditions, reduce the size of the transition table, and under other conditions reduce the string processing time. Given a finite automaton, we can stretch it by transforming each single transition into two or more sequential transitions, thereby introducing additional intermediate states. Jamming is the inverse transformation, in which two or more successive transitions are transformed into a single transition, thereby removing redundant intermediate states. We will present formal definitions of stretching and jamming and we will calculate theoretical bounds, when stretching/jamming is effective in terms of memory consumption.

The Eindhoven FASTAR Days (EFD) 2004 were organized by the Software Construction group of the Department of Mathematics and Computer Science at the Technische Universiteit Eindhoven. On September 3rd and 4th 2004, over thirty participants|hailing from the Czech Republic, Finland, France, The Netherlands, Poland and South Africa|gathered at the Department to attend the EFD. The EFD were organized in connection with the research on finite automata by the FASTAR Research Group, which is centered in Eindhoven and at the University of Pretoria, South Africa. FASTAR (Finite Automata Systems|Theoretical and Applied Research) is an in- ternational research group that aims to lead in all areas related to finite state systems. The work in FASTAR includes both core and applied parts of this field. The EFD therefore focused on the field of finite automata, with an emphasis on practical aspects and applications. Eighteen presentations, mostly on subjects within this field, were given, by researchers as well as students from participating universities and industrial research facilities. This report contains the proceedings of the conference, in the form of papers for twelve of the presentations at the EFD. Most of them were initially reviewed and distributed as handouts during the EFD. After the EFD took place, the papers were revised for publication in these proceedings. We would like to thank the participants for their attendance and presentations, making the EFD 2004 as successful as they were. Based on this success, it is our intention to make the EFD into a recurring event. Eindhoven, December 2004 Loek Cleophas Bruce W. Watson

We show how automaton-based sublinear keyword pattern matching (skpm) algorithms appearing in the literature can be seen as different instantiations of a general automaton-based skpm algorithm skeleton. Such algorithms use finite automata (FA) for efficient computation of string membership in a certain language. The algorithms were formally derived as part of a new skpm algorithm taxonomy, based on an earlier suffix-based skpm algorithm taxonomy [1]. Such a taxonomy is based on deriving the algorithms from a common starting point by successively adding algorithm and problem details and has a number of advantages. It provides correctness arguments, clarifies the working of the algorithms and their interrelationships, helps in implementing the algorithms, and may lead to new algorithms being discovered by finding gaps in the taxonomy. We show how to arrive at the general algorithm skeleton and derive some instantiations, leading to well-known factor- and factor oracle-based algorithms. In doing so, we show the shift functions used for them can be (strengthenings of) shift functions used for suffix-based algorithms. This also results in a number of previously undescribed factor-based skpm algorithm variants, whose performance remains to be investigated.

The theoretical complexity of a string recognizer is linear to the length of the string being tested for acceptance. However, for some kind of strings the processing time largely depends on the number of states visited by the recognizer at run-time. Various experiments are conducted in order to compare the time efficiency of both hardcoded and table-driven algorithms when using such strings patterns. The results of the experiments are cross-compared in order to show the efficiency of the hardcoded algorithm over its table-driven counterpart. This help further the investigations on the problem of the dynamic implementation of finite automata. It is shown that we can rely on the history of the states previously visited in the dynamic framework in order to predict the suitable algorithm for acceptance testing.

A factor oracle is a data structure for weak factor recognition. It is an automaton built on a string p of length m that is acyclic, recognizes at least all factors of p, has m+1 states which are all final, and has m to 2m-1 transitions. In this paper, we give two alternative algorithms for its construction and prove the constructed automata to be equivalent to the automata constructed by the algorithms in [ACR01]. Although these new O(m2) algorithms are practically inefficient compared to the O(m) algorithm given in [ACR01], they give more insight into factor oracles. Our first algorithm constructs a factor oracle based on the suffixes of p in a way that is more intuitive. Some of the crucial properties of factor oracles, which in [ACR01] need several lemmas to be proven, are immediately obvious. Another important property however becomes less obvious. A second algorithm gives a clear insight in the relationship between the trie or dawg recognizing the factors of p and the factor oracle recognizing a superset thereof. We conjecture that an O(m) version of this trie-based algorithm exists.

Traditionally, regular expressions are transformed into (deterministic) finite automata, which are then used in, for example, searching and parsing. For an introduction to automata and regular expressions, refer to [1]. For every automaton, there is an infinite number of other automata that recognizes exactly the same language, although memory usage and performance can differ. This has lead to the wide-spread use of automata minmization techniques. In the same way, for every regular expression, there exists an infinite number of equivalent regular expressions, some of which lead to smaller/faster automata. This paper compares automaton sizes constructed from 10 different regular expressions, both before and after the rewriting transformation. Rewriting is done based on a rule set directly derived from the regular expression language (i.e. Kleene Algebra) axioms; these are listed in Table 1. The first three automata tested are the Thompson NFA [2], the Position NFA [3], and the Follow e-NFA [4]. The remaining three automata are the determinized counterparts of each NFA. For these DFA, the size of the minimized DFA is provided for comparison. For a list of the regular