-
Certified Control for Train Sign Classification
Authors:
Jan Roßbach,
Michael Leuschel
Abstract:
There is considerable industrial interest in integrating AI techniques into railway systems, notably for fully autonomous train systems. The KI-LOK research project is involved in develo** new methods for certifying such AI-based systems. Here we explore the utility of a certified control architecture for a runtime monitor that prevents false positive detection of traffic signs in an AI-based pe…
▽ More
There is considerable industrial interest in integrating AI techniques into railway systems, notably for fully autonomous train systems. The KI-LOK research project is involved in develo** new methods for certifying such AI-based systems. Here we explore the utility of a certified control architecture for a runtime monitor that prevents false positive detection of traffic signs in an AI-based perception system. The monitor uses classical computer vision algorithms to check if the signs -- detected by an AI object detection model -- fit predefined specifications. We provide such specifications for some critical signs and integrate a Python prototype of the monitor with a popular object detection model to measure relevant performance metrics on generated data. Our initial results are promising, achieving considerable precision gains with only minor recall reduction; however, further investigation into generalization possibilities will be necessary.
△ Less
Submitted 16 November, 2023;
originally announced November 2023.
-
Trace Refinement in B and Event-B
Authors:
Sebastian Stock,
Atif Mashkoor,
Michael Leuschel,
Alexander Egyed
Abstract:
Traces are used to show whether a model complies with the intended behavior. A modeler can use trace checking to ensure the preservation of the model behavior during the refinement process. In this paper, we present a trace refinement technique and tool called BERT that allows designers to ensure the behavioral integrity of high-level traces at the concrete level. The proposed technique is evaluat…
▽ More
Traces are used to show whether a model complies with the intended behavior. A modeler can use trace checking to ensure the preservation of the model behavior during the refinement process. In this paper, we present a trace refinement technique and tool called BERT that allows designers to ensure the behavioral integrity of high-level traces at the concrete level. The proposed technique is evaluated within the context of the B and Event-B methods on industrial-strength case studies from the automotive domain.
△ Less
Submitted 28 July, 2022;
originally announced July 2022.
-
Formalization of Advanced VOs semantics and VO Refinement
Authors:
Sebastian Stock,
Fabian Vu,
David Geleßus,
Atif Mashkoor,
Michael Leuschel,
Alexander Egyed
Abstract:
This document lays out the foundations for VO and requirement refinement, abstractions of models, and instantiations. Also, VOs on abstractions and instantiations are considered.
This document lays out the foundations for VO and requirement refinement, abstractions of models, and instantiations. Also, VOs on abstractions and instantiations are considered.
△ Less
Submitted 18 May, 2022;
originally announced May 2022.
-
IVOIRE Deliverable 1.1: Classification of existing VOs & tools and Formalization of VOs semantics
Authors:
Sebastian Stock,
Fabian Vu,
Atif Mashkoor,
Michael Leuschel,
Alexander Egyed
Abstract:
This report discusses the foundations of the VO approach. Then, it explores multiple directions and argues about structure and applications.
This report discusses the foundations of the VO approach. Then, it explores multiple directions and argues about structure and applications.
△ Less
Submitted 12 May, 2022;
originally announced May 2022.
-
Making ProB compatible with SWI-Prolog
Authors:
David Geleßus,
Michael Leuschel
Abstract:
Even though the core of the Prolog programming language has been standardized by ISO since 1995, it remains difficult to write complex Prolog programs that can run unmodified on multiple Prolog implementations. Indeed, implementations sometimes deviate from the ISO standard and the standard itself fails to cover many features that are essential in practice.
Most Prolog applications thus have to…
▽ More
Even though the core of the Prolog programming language has been standardized by ISO since 1995, it remains difficult to write complex Prolog programs that can run unmodified on multiple Prolog implementations. Indeed, implementations sometimes deviate from the ISO standard and the standard itself fails to cover many features that are essential in practice.
Most Prolog applications thus have to rely on non-standard features, often making them dependent on one particular Prolog implementation and incompatible with others. We examine one such Prolog application: ProB, which has been developed for over 20 years in SICStus Prolog.
The article describes how we managed to refactor the codebase of ProB to also support SWI-Prolog, with the goal of verifying ProB's results using two independent toolchains. This required a multitude of adjustments, ranging from extending the SICStus emulation in SWI-Prolog on to better modularizing the monolithic ProB codebase. We also describe notable compatibility issues and other differences that we encountered in the process, and how we were able to deal with them with few major code changes.
Under consideration for acceptance in TPLP.
△ Less
Submitted 9 May, 2022;
originally announced May 2022.
-
Fifty Years of Prolog and Beyond
Authors:
Philipp Körner,
Michael Leuschel,
João Barbosa,
Vítor Santos Costa,
Verónica Dahl,
Manuel V. Hermenegildo,
Jose F. Morales,
Jan Wielemaker,
Daniel Diaz,
Salvador Abreu,
Giovanni Ciatto
Abstract:
Both logic programming in general, and Prolog in particular, have a long and fascinating history, intermingled with that of many disciplines they inherited from or catalyzed. A large body of research has been gathered over the last 50 years, supported by many Prolog implementations. Many implementations are still actively developed, while new ones keep appearing. Often, the features added by diffe…
▽ More
Both logic programming in general, and Prolog in particular, have a long and fascinating history, intermingled with that of many disciplines they inherited from or catalyzed. A large body of research has been gathered over the last 50 years, supported by many Prolog implementations. Many implementations are still actively developed, while new ones keep appearing. Often, the features added by different systems were motivated by the interdisciplinary needs of programmers and implementors, yielding systems that, while sharing the "classic" core language, and, in particular, the main aspects of the ISO-Prolog standard, also depart from each other in other aspects. This obviously poses challenges for code portability. The field has also inspired many related, but quite different languages that have created their own communities.
This article aims at integrating and applying the main lessons learned in the process of evolution of Prolog. It is structured into three major parts. Firstly, we overview the evolution of Prolog systems and the community approximately up to the ISO standard, considering both the main historic developments and the motivations behind several Prolog implementations, as well as other logic programming languages influenced by Prolog. Then, we discuss the Prolog implementations that are most active after the appearance of the standard: their visions, goals, commonalities, and incompatibilities. Finally, we perform a SWOT analysis in order to better identify the potential of Prolog, and propose future directions along which Prolog might continue to add useful features, interfaces, libraries, and tools, while at the same time improving compatibility between implementations.
△ Less
Submitted 14 March, 2022; v1 submitted 26 January, 2022;
originally announced January 2022.
-
Validation Obligations: A Novel Approach to Check Compliance between Requirements and their Formal Specification
Authors:
Atif Mashkoor,
Michael Leuschel,
Alexander Egyed
Abstract:
Traditionally, practitioners use formal methods pre-dominately for one half of the quality-assurance process: verification (do we build the software right?). The other half -- validation (do we build the right software?) -- has been given comparatively little attention. While verification is the core of refinement-based formal methods, where each new refinement step must preserve all properties of…
▽ More
Traditionally, practitioners use formal methods pre-dominately for one half of the quality-assurance process: verification (do we build the software right?). The other half -- validation (do we build the right software?) -- has been given comparatively little attention. While verification is the core of refinement-based formal methods, where each new refinement step must preserve all properties of its abstract model, validation is usually postponed until the latest stages of the development, when models can be automatically executed. Thus mistakes in requirements or in their interpretation are caught too late: usually at the end of the development process. In this paper, we present a novel approach to check compliance between requirements and their formal refinement-based specification during the earlier stages of development. Our proposed approach -- "validation obligations" -- is based on the simple idea that both verification and validation are an integral part of all refinement steps of a system.
△ Less
Submitted 11 February, 2021;
originally announced February 2021.
-
On the Performance of Bytecode Interpreters in Prolog
Authors:
Philipp Körner,
David Schneider,
Michael Leuschel
Abstract:
The semantics and the recursive execution model of Prolog make it very natural to express language interpreters in form of AST (Abstract Syntax Tree) interpreters where the execution follows the tree representation of a program. An alternative implementation technique is that of bytecode interpreters. These interpreters transform the program into a compact and linear representation before evaluati…
▽ More
The semantics and the recursive execution model of Prolog make it very natural to express language interpreters in form of AST (Abstract Syntax Tree) interpreters where the execution follows the tree representation of a program. An alternative implementation technique is that of bytecode interpreters. These interpreters transform the program into a compact and linear representation before evaluating it and are generally considered to be faster and to make better use of resources.
In this paper, we discuss different ways to express the control flow of interpreters in Prolog and present several implementations of AST and bytecode interpreters. On a simple language designed for this purpose, we evaluate whether techniques best known from imperative languages are applicable in Prolog and how well they perform. Our ultimate goal is to assess which interpreter design in Prolog is the most efficient, as we intend to apply these results to a more complex language. However, we believe the analysis in this paper to be of more general interest.
△ Less
Submitted 28 August, 2020;
originally announced August 2020.
-
Prolog for Verification, Analysis and Transformation Tools
Authors:
Michael Leuschel
Abstract:
This article examines the use of the Prolog language for writing verification, analysis and transformation tools. Guided by experience in teaching and the development of verification tools like ProB or specialisation tools like ECCE and LOGEN, the article presents an assessment of various aspects of Prolog and provides guidelines for using them. The article shows the usefulness of a few key Prolo…
▽ More
This article examines the use of the Prolog language for writing verification, analysis and transformation tools. Guided by experience in teaching and the development of verification tools like ProB or specialisation tools like ECCE and LOGEN, the article presents an assessment of various aspects of Prolog and provides guidelines for using them. The article shows the usefulness of a few key Prolog features. In particular, it discusses how to deal with negation at the level of the object programs being verified or analysed.
△ Less
Submitted 6 August, 2020;
originally announced August 2020.
-
Constraint Logic Programming over Infinite Domains with an Application to Proof
Authors:
Sebastian Krings,
Michael Leuschel
Abstract:
We present a CLP(FD)-based constraint solver able to deal with unbounded domains. It is based on constraint propagation, resorting to enumeration if all other methods fail. An important aspect is detecting when enumeration was complete and if this has an impact on the soundness of the result. We present a technique which guarantees soundness in the following way: if the constraint solver finds a s…
▽ More
We present a CLP(FD)-based constraint solver able to deal with unbounded domains. It is based on constraint propagation, resorting to enumeration if all other methods fail. An important aspect is detecting when enumeration was complete and if this has an impact on the soundness of the result. We present a technique which guarantees soundness in the following way: if the constraint solver finds a solution it is guaranteed to be correct; if the constraint solver fails to find a solution it can either return the result "definitely false" in case it knows enumeration was exhaustive, or "unknown" in case it was aborted. The technique can deal with nested universal and existential quantifiers. It can easily be extended to set comprehensions and other operators introducing new quantified variables. We show applications in data validation and proof.
△ Less
Submitted 3 January, 2017;
originally announced January 2017.
-
Knowledge Representation Analysis of Graph Mining
Authors:
Matthias van der Hallen,
Sergey Paramonov,
Michael Leuschel,
Gerda Janssens
Abstract:
Many problems, especially those with a composite structure, can naturally be expressed in higher order logic. From a KR perspective modeling these problems in an intuitive way is a challenging task. In this paper we study the graph mining problem as an example of a higher order problem. In short, this problem asks us to find a graph that frequently occurs as a subgraph among a set of example graph…
▽ More
Many problems, especially those with a composite structure, can naturally be expressed in higher order logic. From a KR perspective modeling these problems in an intuitive way is a challenging task. In this paper we study the graph mining problem as an example of a higher order problem. In short, this problem asks us to find a graph that frequently occurs as a subgraph among a set of example graphs. We start from the problem's mathematical definition to solve it in three state-of-the-art specification systems. For IDP and ASP, which have no native support for higher order logic, we propose the use of encoding techniques such as the disjoint union technique and the saturation technique. ProB benefits from the higher order support for sets. We compare the performance of the three approaches to get an idea of the overhead of the higher order support.
We propose higher-order language extensions for IDP-like specification languages and discuss what kind of solver support is needed. Native higher order shifts the burden of rewriting specifications using encoding techniques from the user to the solver itself.
△ Less
Submitted 31 August, 2016;
originally announced August 2016.
-
Symbolic Reachability Analysis of B through ProB and LTSmin
Authors:
Jens Bendisposto,
Philipp Koerner,
Michael Leuschel,
Jeroen Meijer,
Jaco van de Pol,
Helen Treharne,
Jorden Whitefield
Abstract:
We present a symbolic reachability analysis approach for B that can provide a significant speedup over traditional explicit state model checking. The symbolic analysis is implemented by linking ProB to LTSmin, a high-performance language independent model checker. The link is achieved via LTSmin's PINS interface, allowing ProB to benefit from LTSmin's analysis algorithms, while only writing a few…
▽ More
We present a symbolic reachability analysis approach for B that can provide a significant speedup over traditional explicit state model checking. The symbolic analysis is implemented by linking ProB to LTSmin, a high-performance language independent model checker. The link is achieved via LTSmin's PINS interface, allowing ProB to benefit from LTSmin's analysis algorithms, while only writing a few hundred lines of glue-code, along with a bridge between ProB and C using ZeroMQ. ProB supports model checking of several formal specification languages such as B, Event-B, Z and TLA. Our experiments are based on a wide variety of B-Method and Event-B models to demonstrate the efficiency of the new link. Among the tested categories are state space generation and deadlock detection; but action detection and invariant checking are also feasible in principle. In many cases we observe speedups of several orders of magnitude. We also compare the results with other approaches for improving model checking, such as partial order reduction or symmetry reduction. We thus provide a new scalable, symbolic analysis algorithm for the B-Method and Event-B, along with a platform to integrate other model checking improvements via LTSmin in the future.
△ Less
Submitted 14 March, 2016;
originally announced March 2016.
-
Checking Computations of Formal Method Tools - A Secondary Toolchain for ProB
Authors:
John Witulski,
Michael Leuschel
Abstract:
We present the implementation of pyB, a predicate - and expression - checker for the B language. The tool is to be used for a secondary tool chain for data validation and data generation, with ProB being used in the primary tool chain. Indeed, pyB is an independent cleanroom-implementation which is used to double-check solutions generated by ProB, an animator and model-checker for B specification…
▽ More
We present the implementation of pyB, a predicate - and expression - checker for the B language. The tool is to be used for a secondary tool chain for data validation and data generation, with ProB being used in the primary tool chain. Indeed, pyB is an independent cleanroom-implementation which is used to double-check solutions generated by ProB, an animator and model-checker for B specifications. One of the major goals is to use ProB together with pyB to generate reliable outputs for high-integrity safety critical applications. Although pyB is still work in progress, the ProB/pyB toolchain has already been successfully tested on various industrial B machines and data validation tasks.
△ Less
Submitted 26 April, 2014;
originally announced April 2014.
-
Who watches the watchers: Validating the ProB Validation Tool
Authors:
Jens Bendisposto,
Sebastian Krings,
Michael Leuschel
Abstract:
Over the years, ProB has moved from a tool that complemented proving, to a development environment that is now sometimes used instead of proving for applications, such as exhaustive model checking or data validation. This has led to much more stringent requirements on the integrity of ProB. In this paper we present a summary of our validation efforts for ProB, in particular within the context of t…
▽ More
Over the years, ProB has moved from a tool that complemented proving, to a development environment that is now sometimes used instead of proving for applications, such as exhaustive model checking or data validation. This has led to much more stringent requirements on the integrity of ProB. In this paper we present a summary of our validation efforts for ProB, in particular within the context of the norm EN 50128 and safety critical applications in the railway domain.
△ Less
Submitted 26 April, 2014;
originally announced April 2014.
-
Formally Checking Large Data Sets in the Railways
Authors:
Thierry Lecomte,
Lilian Burdy,
Michael Leuschel
Abstract:
This article presents industrial experience of validating large data sets against specification written using the B / Event-B mathematical language and the ProB model checker.
This article presents industrial experience of validating large data sets against specification written using the B / Event-B mathematical language and the ProB model checker.
△ Less
Submitted 25 October, 2012; v1 submitted 25 October, 2012;
originally announced October 2012.
-
Constraint-Based Deadlock Checking of High-Level Specifications
Authors:
Stefan Hallerstede,
Michael Leuschel
Abstract:
Establishing the absence of deadlocks is important in many applications of formal methods. The use of model checking for finding deadlocks in formal models is often limited. In this paper we propose a constraint-based approach to finding deadlocks employing the ProB constraint solver. We present the general technique, as well as various improvements that had to be performed on ProB's Prolog kernel…
▽ More
Establishing the absence of deadlocks is important in many applications of formal methods. The use of model checking for finding deadlocks in formal models is often limited. In this paper we propose a constraint-based approach to finding deadlocks employing the ProB constraint solver. We present the general technique, as well as various improvements that had to be performed on ProB's Prolog kernel, such as reification of membership and arithmetic constraints. This work was guided by an industrial case study, where a team from Bosch was modeling a cruise control system. Within this case study, ProB was able to quickly find counter examples to very large deadlock-freedom constraints. In the paper, we also present other successful applications of this new technique. Experiments using SAT and SMT solvers on these constraints were thus far unsuccessful.
△ Less
Submitted 9 September, 2011;
originally announced September 2011.
-
A Semantics-Aware Editing Environment for Prolog in Eclipse
Authors:
Jens Bendisposto,
Ian Endrijautzki,
Michael Leuschel,
David Schneider
Abstract:
In this paper we present a Prolog plugin for Eclipse based upon BE4, and providing many features such as semantic-aware syntax highlighting, outline view, error marking, content assist, hover information, documentation generation, and quick fixes. The plugin makes use of a Java parser for full Prolog with an integrated Prolog engine, and can be extended with further semantic analyses, e.g., base…
▽ More
In this paper we present a Prolog plugin for Eclipse based upon BE4, and providing many features such as semantic-aware syntax highlighting, outline view, error marking, content assist, hover information, documentation generation, and quick fixes. The plugin makes use of a Java parser for full Prolog with an integrated Prolog engine, and can be extended with further semantic analyses, e.g., based on abstract interpretation.
△ Less
Submitted 12 March, 2009;
originally announced March 2009.
-
Improving Size-Change Analysis in Offline Partial Evaluation
Authors:
Michael Leuschel,
Salvador Tamarit,
German Vidal
Abstract:
Some recent approaches for scalable offline partial evaluation of logic programs include a size-change analysis for ensuring both so called local and global termination. In this work|inspired by experimental evaluation|we introduce several improvements that may increase the accuracy of the analysis and, thus, the quality of the associated specialized programs. We aim to achieve this while mainta…
▽ More
Some recent approaches for scalable offline partial evaluation of logic programs include a size-change analysis for ensuring both so called local and global termination. In this work|inspired by experimental evaluation|we introduce several improvements that may increase the accuracy of the analysis and, thus, the quality of the associated specialized programs. We aim to achieve this while maintaining the same complexity and scalability of the recent works.
△ Less
Submitted 12 March, 2009;
originally announced March 2009.
-
Offline Specialisation in Prolog Using a Hand-Written Compiler Generator
Authors:
Michael Leuschel,
Jesper Joergensen,
Wim Vanhoof,
Maurice Bruynooghe
Abstract:
The so called ``cogen approach'' to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success in partial evaluation of both functional and imperative languages. This paper demonstrates that the cogen approach is also applicable to the specialisation of logic programs (also called partial deduction) and leads to effective specialisers.…
▽ More
The so called ``cogen approach'' to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success in partial evaluation of both functional and imperative languages. This paper demonstrates that the cogen approach is also applicable to the specialisation of logic programs (also called partial deduction) and leads to effective specialisers. Moreover, using good binding-time annotations, the speed-ups of the specialised programs are comparable to the speed-ups obtained with online specialisers. The paper first develops a generic approach to offline partial deduction and then a specific offline partial deduction method, leading to the offline system LIX for pure logic programs. While this is a usable specialiser by itself, it is used to develop the cogen system LOGEN. Given a program, a specification of what inputs will be static, and an annotation specifying which calls should be unfolded, LOGEN generates a specialised specialiser for the program at hand. Running this specialiser with particular values for the static inputs results in the specialised program. While this requires two steps instead of one, the efficiency of the specialisation process is improved in situations where the same program is specialised multiple times. The paper also presents and evaluates an automatic binding-time analysis that is able to derive the annotations. While the derived annotations are still suboptimal compared to hand-crafted ones, they enable non-expert users to use the LOGEN system in a fully automated way. Finally, LOGEN is extended so as to directly support a large part of Prolog's declarative and non-declarative features and so as to be able to perform so called mixline specialisations.
△ Less
Submitted 7 August, 2002;
originally announced August 2002.
-
Logic program specialisation through partial deduction: Control issues
Authors:
Michael Leuschel,
Maurice Bruynooghe
Abstract:
Program specialisation aims at improving the overall performance of programs by performing source to source transformations. A common approach within functional and logic programming, known respectively as partial evaluation and partial deduction, is to exploit partial knowledge about the input. It is achieved through a well-automated application of parts of the Burstall-Darlington unfold/fold t…
▽ More
Program specialisation aims at improving the overall performance of programs by performing source to source transformations. A common approach within functional and logic programming, known respectively as partial evaluation and partial deduction, is to exploit partial knowledge about the input. It is achieved through a well-automated application of parts of the Burstall-Darlington unfold/fold transformation framework. The main challenge in develo** systems is to design automatic control that ensures correctness, efficiency, and termination. This survey and tutorial presents the main developments in controlling partial deduction over the past 10 years and analyses their respective merits and shortcomings. It ends with an assessment of current achievements and sketches some remaining research challenges.
△ Less
Submitted 12 February, 2002;
originally announced February 2002.
-
A Polyvariant Binding-Time Analysis for Off-line Partial Deduction
Authors:
Maurice Bruynooghe,
Michael Leuschel,
Konstantinos Sagonas
Abstract:
We study the notion of binding-time analysis for logic programs. We formalise the unfolding aspect of an on-line partial deduction system as a Prolog program. Using abstract interpretation, we collect information about the run-time behaviour of the program. We use this information to make the control decisions about the unfolding at analysis time and to turn the on-line system into an off-line s…
▽ More
We study the notion of binding-time analysis for logic programs. We formalise the unfolding aspect of an on-line partial deduction system as a Prolog program. Using abstract interpretation, we collect information about the run-time behaviour of the program. We use this information to make the control decisions about the unfolding at analysis time and to turn the on-line system into an off-line system. We report on some initial experiments.
△ Less
Submitted 17 March, 2000;
originally announced March 2000.
