Published in International Journal on Software Tools for Technology Transfer
Parametric timed automata (PTAs) are a powerful formalism to reason, simulate and formally verify critical real-time systems. After 25 years of research on PTAs, it is now well understood that any non-trivial problem studied is undecidable for general PTAs. We provide here a survey of decision and computation problems for PTAs. On the one hand, bou...
Published in International Journal on Software Tools for Technology Transfer
Published in International Journal on Software Tools for Technology Transfer
Sketching is a synthesis approach that allows users to provide high-level insights into a synthesis problem and let synthesis tools complete low-level details. Users write sketches—partial programs that have “holes” and provide test assertions as the correctness criteria. The sketching techniques fill the holes with code fragments such that the com...
Published in International Journal on Software Tools for Technology Transfer
Read–copy update (RCU) is a synchronization mechanism used heavily in key components of the Linux kernel, such as the virtual filesystem (VFS), to achieve scalability by exploiting RCU’s ability to allow concurrent reads and updates. RCU’s design is non-trivial, requires a significant effort to fully understand it, let alone become convinced that i...
Published in International Journal on Software Tools for Technology Transfer
In the automata theoretic approach to explicit state LTL model checking, the synchronized product of the model and an automaton that represents the negated formula is checked for emptiness. In practice, a (transition-based generalized) Büchi automaton (TGBA) is used for this procedure. This paper investigates whether using a more general form of ac...
Published in International Journal on Software Tools for Technology Transfer
Parity games play an important role in model checking and synthesis. In their paper, Calude et al. have recently shown that these games can be solved in quasi-polynomial time. We show that their algorithm can be implemented efficiently: we use their data structure as a progress measure, allowing for a backward implementation instead of a complete u...
Published in International Journal on Software Tools for Technology Transfer
Model-driven code checking (MDCC) has been successfully used for the verification of functional requirements of C code. An environment model that describes the context, which a program is expected to run in, is defined in Promela, translated to a model checker program by Spin, and linked with the program acting as system under verification. In this...
Published in International Journal on Software Tools for Technology Transfer
The quantitative analysis of concurrent systems requires expressive and user-friendly property languages combining temporal, data handling, and quantitative aspects. In this paper, we aim at facilitating the quantitative analysis of systems modeled as PTSs (Probabilistic Transition Systems) labeled by actions containing data values and probabilitie...
Published in International Journal on Software Tools for Technology Transfer
Software quality assurance aims to ensure that the software product meets the quality standards expected by the customer. This special issue of Software Tools for Technology Transfer is concerned with the foundations on which software quality assurance is built. It introduces the papers that focus on this topic and that have been selected from the ...
Published in International Journal on Software Tools for Technology Transfer
We present an approach for hybrid systems that combines the advantages of component-based modeling (e.g., reduced model complexity) with the advantages of formal verification (e.g., guaranteed contract compliance). Component-based modeling can be used to split large models into multiple component models with local responsibilities to reduce modelin...
