View: session overviewtalk overview
10:30 | Relating Alternating Relations for Conformance and Refinement PRESENTER: Frits Vaandrager ABSTRACT. Various relations have been defined to express refinement and conformance for state-transition systems with inputs and outputs, such as ioco and uioco in the area of model-based testing, and alternating simulation and alternating-trace containment originating from game theory and formal verification. Several papers have compared these independently developed relations, but these comparisons make assumptions (such as input-enabledness), pose restrictions (such as determinism -- then they all coincide), use different models (such as interface automata and Kripke structures), or do not deal with the concept of quiescence. In this paper, we present the integration of the ioco/uioco theory of model-based testing and the theory of alternating refinements, within the domain of non-deterministic, non-input-enabled interface automata. A standing conjecture is that ioco and alternating trace containment coincide. Our main result is that this conjecture does not hold, but that uioco coincides with a variant of alternating-trace containment, for image finite interface automata and with explicit treatment of quiescence. This result is based on a particular translation of the game-theoretic notion of alternating-trace containment from Kripke structures to the setting of interface automata. From the comparison between ioco-theory and alternating refinements, we conclude that ioco and the original relation of alternating trace containment are too strong for realistic black-box scenarios. |
11:00 | A Multi-Target Code Generator for High-Level B PRESENTER: Fabian Vu ABSTRACT. In the traditional workflow of high-level specification languages such as B, code is refined in many steps until a small "implementable" subset of the language is reached. Then, code generators are used to derive code from this implementation-level code, targeting traditional programming languages such as C or Ada. In this paper, we pursue the aim to diminish the number of refinement steps needed, by providing a more powerful code generator. Indeed, many high-level data types and operations, such as sets, can already be translated to traditional programming languages such as Java and C++. We present a new code generator for B named B2Program with two distinct features. Firstly, it targets multiple high-level languages via a template-based approach to compilation. In addition to flexibility, this also enables one to safeguard against errors in the individual compilers and standard libraries, by generating multiple implementations of the same formal model. Secondly, it supports higher-level constructs compared to existing code generators. This enables new uses of formal models, as prototypes, demonstrators or simply as very high-level programming languages for productivity gains, by directly embedding formal models as components into software systems. In the article, we discuss the implementation of our code generator, evaluate it using B models taken from literature and compare its performance with simulation in ProB. |
11:30 | Embedding SMT-LIB into B for Interactive Proof and Constraint Solving PRESENTER: Sebastian Krings ABSTRACT. The SMT-LIB language and the B language are both basedon predicate logic and share the definition of several operators. However, B supports data types not available in SMT-LIB and vice versa. In this article we suggest a straightforward translation from SMT-LIB to B. Using this translation, SMT-LIB can be analyzed by tools developed for the B method. We show how Atelier B can be used for automatic and interactive proof of SMT-LIB problems. Furthermore, we incorporated our translation into the model checker ProB and applied it to several benchmarks taken from the SMT-LIB repository. In contrast to most SMT solvers, ProB relies on finite domain constraint propagation, with support for infinite domains by keeping track of the exhaustiveness of domain variable enumerations. Our goal was to see whether this kind of approach is beneficial for SMT solving. |
10:30 | Sound Probabilistic Numerical Error Analysis PRESENTER: Debasmita Lohar ABSTRACT. Numerical software uses floating-point arithmetic to implement real-valued algorithms which inevitably introduces roundoff errors. Additionally, in an effort to reduce energy consumption, approximate hardware introduces further errors. As errors are propagated through a computation, the result of the approximated floating-point program can be vastly different from the real-valued ideal one. Previous work on soundly bounding (roundoff) errors has focused on worst-case absolute error analysis. However, not all inputs and not all errors are equally likely such that these methods can lead to overly pessimistic error bounds. In this paper, we present a sound probabilistic static analysis which takes into account the probability distributions of inputs and propagates roundoff and approximation errors probabilistically through the program. We observe that the computed probability distributions of errors are hard to interpret, and propose an alternative metric and computation of refined error bounds which are valid with some probability. |
11:00 | Computing Bisimilarity Metrics for Probabilistic Timed Automata PRESENTER: Simone Tini ABSTRACT. We are interested in describing timed systems that exhibit probabilistic behaviour and in evaluating their behavioural discrepancies. To this purpose, we consider probabilistic timed automata, we introduce a concept of $n$-bisimilarity metric and give an algorithm to decide it. |
11:30 | Ontology-Mediated Probabilistic Model Checking PRESENTER: Clemens Dubslaff ABSTRACT. Probabilistic model checking (PMC) is a well-established method for the quantitative analysis of dynamic systems. On the other hand, description logics (DLs) provide a well-suited formalism to describe and reason about static knowledge, used in many areas to specify domain knowledge in an ontology. We investigate how such knowledge can be integrated into the PMC process, introducing ontology-mediated PMC. Specifically, we propose a formalism that links ontologies to dynamic behaviors specified by guarded commands, the de-facto standard input formalism for PMC tools such as Prism. Further, we present and implement a technique for their analysis relying on existing DL-reasoning and PMC tools. This way, we enable the application of standard PMC techniques to analyze knowledge-intensive systems. Our approach is implemented and evaluated on a multi-server system case study, where different DL-ontologies are used to provide specifications of different server platforms and situations the system is executed in. |