2013
Validation of Formal Models by Refinement Animation
[PDF] [Bibtex]Science of Computer Programming, 78(3): 272-292, 2013.
We provide a detailed description of refinement in Event-B, both as a contribution in itself and as a foundation for the approach to simultaneous animation of multiple levels of refinement that we propose. We present an algorithm for simultaneous multi-level animation of refinement, and show how it can be used to detect a variety of errors that occur frequently when using refinement. The algorithm has been implemented in ProB and we applied it to several case studies, showing that multi-level animation is tractable also on larger models. We present empirical results and discuss how the algorithm can be combined with symmetry reduction.
In Managing Requirements Knowledge, Springer, 2013.
This chapter presents the the Requirements Modeling Framework (RMF), an Eclipse-based open source platform for requirements engineering. The core of RMF is based on the emerging Requirements Interchange Format (ReqIF), which is an OMG standard. The project uses ReqIF as the central data model. At the time of this writing, RMF was the only open source implementation of the ReqIF data model.
By being based on an open standard that is currently gaining industry support, RMF can act as an interface to existing requirements management tools. Further, by based on the Eclipse platform, integration with existing Eclipse-based offerings is possible.
In this chapter, we will describe the architecture of the RMF project, as well as the underlying ReqIF standard. Further, we give an overview of the GUI, which is called ProR. A key strength of RMF and ProR is the extensibility, and we present the integration ProR with Rodin, which allows traceability between natural language requirements and Event-B formal models.
A Method and Tool for Tracing Requirements into Specifications
[PDF] [Bibtex]Submitted to Science of Computer Programming
The creation of a consistent system description is a challenging problem of requirements engineering. Formal and informal reasoning can greatly contribute to meet this challenge. However, this demands that formal and informal reasoning and the system description are connected in such way that the reasoning permits drawing conclusions about the system description.
We describe an incremental approach to requirements modelling and validation that incorporates formal and informal reasoning. Our main contribution is an approach to requirements tracing that delivers the necessary connection that links the reasoning to the system description. Formal refinement is used in order to deal with large and complex system descriptions.
We discuss tool support for our approach of requirements tracing that combines informal requirements modelling with formal modelling and verification while tracing requirements among each other and into the formal model.
2012
CoRR, abs/1210.6815, 2012.
The ProR Approach: Traceability of Requirements and System Descriptions
[PDF] [Bibtex]CreateSpace, 2012.
Creating a system description of high quality is still a challenging problem in the field of requirements engineering. Creating a formal system description addresses some issues. However, the relationship of the formal model to the user requirements is rarely clear, or documented satisfactorily.
This work presents the ProR approach, an approach for the creation of a consistent system description from an initial set of requirements. The resulting system description is a mixture of formal and informal artefacts. Formal and informal reasoning is employed to aid in the process. To achieve this, the artefacts must be connected by traces to support formal and informal reasoning, so that conclusions about the system description can be drawn.
The ProR approach enables the incremental creation of the system description, alternating between modelling (both formal and informal) and validation. During this process, the necessary traceability for reasoning about the system description is established. The formal model employs refinement for further structuring of large and complex system descriptions. The development of the ProR approach is the first contribution of this work.
This work also presents ProR, a tool platform for requirements engineering, that supports the ProR approach. ProR has been integrated with Rodin, a tool for Event-B modelling, to provide a number of features that allow the ProR approach to scale.
The core features of ProR are independent from the ProR approach. The data model of ProR builds on the international ReqIF standard, which provides interoperability with industrial tools for requirements engineering. The development of ProR created enough interest to justify the creation of the Requirements Modeling Framework (RMF), a new Eclipse Foundation project, which is the open source host for ProR. RMF attracted an active community, and ProR development continues. The development of ProR is the second contribution of this work.
This work is accompanied by a case study of a traffic light system, which demonstrates the application of both the ProR approach and ProR.
In Proceedings FM'2012, LNCS 7436, Springer, 2012.
We present the integration of the Kodkod high-level interface to SAT-solvers into the kernel of ProB. As such, predicates from B, Event-B, Z and TLA+ can be solved using a mixture of SAT-solving and ProB's own constraint-solving capabilities developed using constraint logic programming: the first-order parts which can be dealt with by Kodkod and the remaining parts solved by the existing ProB kernel. We also present an extensive empirical evaluation and analyze the respective merits of SAT-solving and classical constraint solving. We also compare to using SMT solvers via recently available translators for Event-B.
In Proceedings iFM'2012, LNCS 7321, Springer, 2012.
TLA+ and B share the common base of predicate logic, arithmetic and set theory. However, there are still considerable differences, such as very different approaches to typing and modularization. There is also considerable difference in the available tool support. In this paper, we present a translation of the non-temporal part of TLA+ to B, which makes it possible to feed TLA+ specifications into existing tools for B. Part of this translation must include a type inference algorithm, in order to produce typed B specifications. There are many other tricky aspects, such as translating modules as well as let and if-then-else expressions. We also present an integration of our translation into ProB. ProB thus provides a complementary tool to the explicit state model checker TLC, with convenient animation and constraint solving for TLA+. We also present a series of case studies, highlighting the complementarity to TLC. In particular, we highlight the sometimes dramatic difference in performance when it comes to solving complicated constraints in TLA+.
The Efficient Handling of Guards in the Design of RPython’s Tracing JIT
[PDF] [Bibtex]In VMIL, accepted for publication, 2012.
Tracing just-in-time (JIT) compilers record linear control flow paths, inserting operations called guards at points of possible divergence. These operations occur frequently in generated traces and therefore it is important to design and implement them carefully to find the right trade-off between deoptimization, memory overhead, and (partly) execution speed. In this paper, we perform an empirical analysis of runtime properties of guards. This is used to guide the design of guards in the RPython tracing JIT.
In DLS, 2012.
One of the nice properties of a tracing just-in-time compiler (JIT) is that many of its optimizations are simple, requiring one forward pass only. This is not true for loop-invariant code motion which is a very important optimization for code with tight kernels. Especially for dynamic languages that typically perform quite a lot of loop invariant type checking, boxed value unwrapping and virtual method lookups.
In this paper we explain a scheme pioneered within the context of the LuaJIT project for making basic optimizations loop-aware by using a simple pre-processing step on the trace without changing the optimizations themselves.
We have implemented the scheme in RPython's tracing JIT compiler. PyPy's Python JIT executing simple numerical kernels can become up to two times faster, bringing the performance into the ballpark of static language compilers.
A Systems Engineering Tool Chain Based on Eclipse and Rodin
[PDF] [Bibtex]In Forms/Format, 2012.
ReqIF: Seamless Requirements Interchange Format between Business Partners
[PDF] [Bibtex]In IEEE Software, 2012.
The primary sources of project risks and product problems are poor, missing, or changing requirements. Often, the underlying root cause is insufficient collaboration between business partners. This article provides insight into how to effectively collaborate in requirements engineering. We describe the Requirements Interchange Format (ReqIF) standard and technologies for seamless requirements development and management. We look forward to hearing from both readers and prospective column authors about this and the technologies and tools you want to know more about.
Architectures for an Extensible Text Editor for Rodin
[PDF] [Bibtex]Technical Report, University of Düsseldorf, 2012.
Rodin is a platform for Event-B modelling. Its native editor is a structural editor that allows the modification of a tree-like model.
Especially for large models, some users found the default editor inadequate and preferred a text-based editor. Such an editor, called Camille, was created by Fabian Fritz in 2009 and was a huge success.
Nevertheless, Camille does not directly support extensions for Rodin. As more and more extensions are being created, this became a larger issue over the years.
This report analyses how Camille extensibility can be achieved. It analyses a number of different architectures and compares their mutual advantages and disadvantages.
This paper discusses four different approaches. Out of these, we find two particularly promising. The first option would be the implementation of a block parser that provides a useful default implementation for plug-in developers and a pleasing syntax to editor users. The second option is the use of an existing syntax like YAML. This solution could be extended all the way to the persistence layer of Rodin, thereby simplifying the back end significantly. But such an effort would require additional resources. Nevertheless, the result would simplify maintenance of the platform significantly in the long run.
ReqIF – the new Requirements Standard and its Open Source implementation Eclipse RMF
[Bibtex]Technical Report, Commercial Vehicle Technology Symposium, 2012.
Requirements Traceability between Textual Requirements and Formal Models Using ProR
[PDF] [Bibtex]Accepted for iFM'2012
Traceability within a system description is a challenging problem of requirements engineering. In particular, formal models of the system are often based on informal requirements, but creating and maintaining the traceability between the two can be challenging. Previously, we presented an incremental approach for producing a system description from an initial set of requirements. The foundation of the approach is a classification of requirements into artefacts W (domain properties), R (requirements) and S (specification). In addition, the approach uses designated phenomena as the vocabulary employed by the artefacts. The central idea is that adequacy of the system description must be justified, meaning that W /\ S => R. The approach establishes a traceability, and the resulting system description may consist of formal and informal artefacts.
We created tool support for this approach by integrating Rodin and ProR ...
2011
Automated Property Verification for Large Scale B Models with ProB
[PDF] [Bibtex]Formal Aspects of Computing, 23(6): 683-709, 2011.
In this paper we describe the successful application of the ProB validation tool for several industrial applications. The initial case study centred on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for Atelier B. Atelier B, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense (and they need to be revalidated whenever the rail network infrastructure changes).
In this paper we show how we were able to use ProB to validate all of the about 300 properties of the San Juan deployment, detecting exactly the same faults automatically in a few minutes that were manually uncovered in about one man-month. We have repeated this task for three ongoing projects at Siemens, notably the ongoing automatisation of the line 1 of the Paris Metro. Here again, about a man month of effort has been replaced by a few minutes of computation.
This achievement required the extension of the ProB kernel for large sets as well as an improved constraint propagation phase. We also outline some of the effort and features that were required in moving from a tool capable of dealing with medium-sized examples towards a tool able to deal with actual industrial specifications. We also describe the issue of validating ProB, so that it can be integrated into the SIL4 development chain at Siemens.
Constraint-Based Deadlock Checking of High-Level Specifications
[PDF] [Bibtex]Theory and Practice of Logic Programming, 11(4-5): 767-782, 2011.
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 limited because in many industrial applications the state space is either infinite or much too large to be explored exhaustively.
In this paper we propose a constraint-based approach to finding deadlocks employing the ProB constraint solver to find values for the constants and variables of formal models that describe a deadlocking state. 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.
ProB typically finds counter examples to deadlock-freedom constraints, a formula of about 900 partly nested conjunctions and disjunction among them 80 arithmetic and 150 set-theoretic predicates (in total a formula of 30 pages), in under two seconds.
We also present other successful applications of this new technique, in particular to BPEL processes. Experiments using SAT and SMT solvers on these constraints were thus far unsuccessful.
Developing Camille, a text editor for Rodin
[Bibtex]Software: Practice and Experience, 41(2): 189-198, 2011.
Initially, the Rodin platform for Event-B did away with a textual representation for models. In this paper, we explain why a textual representation was required after all and we present the semantic-aware text editor Camille for Rodin. We explain the design choices of Camille, such as splitting the syntax into two-levels for machine and formula syntax. We also describe the challenges, such as synchronizing the textual representation with the Rodin database, and how they were overcome using an EMF abstraction layer.
ProR - Eine Softwareplattform für Requirements Engineering
[PDF] [Bibtex]Softwaretechnik-Trends, 31(1), 2011.
Gute Werkzeugunterstützung ist ein wichtiger Aspekt im Requirements Engineering. Es gibt zwar ein breites kommerzielles Angebot, aber wenige offene Lösungen. ProR ist eine OpenSource Software zum Arbeiten mit natürlichsprachigen Anforderungen. Es basiert auf dem Requirements Interchange Format (RIF), womit wir die Interoperabilität mit anderen Werkzeugen gewährleisten. Wir legen großen Wert auf die Erweiterbarkeit der Plattform, was wir mit einem Integrations-Plugin für die formale Event-B-Methode belegen.
Requirement Traceability in Topcased with the Requirements Interchange Format (RIF/ReqIF)
[PDF] [Bibtex]First Topcased Days Toulouse, 2011.
One important step of the systems engineering process is requirements engineering. Parallel to the development of Topcased, which includes tooling for requirements engineering, a new standard for requirements exchange is emerging at the OMG under the name “ReqIF” (formally called RIF). In our talk we introduce the activities of two research projects and their tool developments, VERDE (Yakindu Requirements) and Deploy (ProR) and discuss possible synergies with Topcased.
Finding Deadlocks of Event-B Models by Constraint Solving
[PDF] [Bibtex]In B2011 Workshop (short paper), 2011.
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 limited because in many industrial applications the state space is either infinite or much too large to be explored exhaustively. In this paper we propose a constraint-based approach to finding deadlocks employing the ProB constraint solver to find values for the constants and variables of formal models that describe a deadlocking state. We discuss the principles of the technique implemented in ProB's Prolog kernel and present some results of a larger case study to which we have applied the approach.
In Proceedings of Fundamental Approaches to Software Engineering (FASE) 2011, volume 6603 of Lecture Notes in Computer Science, Springer, 2011.
In Event-B a system is developed using refinement. The language is based on a relatively small core; in particular there is only a very small number of substitutions. This results in much simpler proof obligations, that can be handled by automatic tools. However, the downside is that, in case of software development, structural information is not explicitly available but hidden in the chain of refinements. This paper discusses a method to uncover these implicit algorithmic structures and use them in a model checker. Other applications are code generation, model comprehension, and testcase generation.
Mixing Formal and Informal Model Elements for Tracing Requirements
[PDF] [Bibtex]In booktitle, AVOCS 2011, 2011.
Tracing between informal requirements and formal models is challenging. A method for such tracing should permit to deal efficiently with changes to both the requirements and the model. A particular challenge is posed by the persisting interplay of formal and informal elements.
In this paper, we describe an incremental approach to requirements validation and systems modelling. Formal modelling facilitates a high degree of automation: it serves for validation and traceability.
The foundation for our approach are requirements that are structured according to the WRSPM reference model. We provide a system for traceability with a state-based formal method that supports refinement. We do not require all specification elements to be modelled formally and support incremental incorporation of new specification elements into the formal model. Refinement is used to deal with larger amounts of requirements in a structured way.
We provide a small example using Problem Frames and Event-B to demonstrate our approach.
In Proceedings ICFEM'2011, volume 6991 of Lecture Notes in Computer Science, Springer, 2011.
The development of the Event-B formal method and the supporting tools Rodin and ProB was guided by practical experiences with the B-Method, the Z specification notation, VDM and similar practical formal methods. The case study discussed in this article - a cruise control system - is a serious test of industrial use. We report on where Event-B and its tools have succeeded, where they have not. We also report on advances that were inspired by the case study. Interestingly, the case study was not a pure formal methods problem. In addition to Event-B, it used Problem Frames for capturing requirements. The interaction between the two proved to be crucial for the success of the case study. The heart of the problem was tracing informal requirements from Problem Frames descriptions to formal Event-B models. To a large degree, this issue dictated the approach that had to be used for formal modelling. A dedicated record theory and dedicated tool support were required. The size of the formal models rather than complex individual formulas was the main challenge for tool support.
Runtime Feedback in a Meta-Tracing JIT for Efficient Dynamic Languages
[PDF] [Bibtex]In Proceedings of the 6th workshop on the Implementation, Compilation, Optimization of Object-Oriented Languages and Programming Systems series = ICOOOLPS '11, 2011.
Meta-tracing JIT compilers can be applied to a variety of differ- ent languages without explicitly encoding language semantics into the compiler. So far, they lacked a way to give the language im- plementor control over runtime feedback. This restricted their per- formance. In this paper we describe the mechanisms in PyPy’s meta-tracing JIT that can be used to control runtime feedback in language-specific ways. These mechanisms are flexible enough to express classical VM techniques such as maps and runtime type feedback.
Allocation removal by partial evaluation in a tracing JIT
[PDF] [Bibtex]In PEPM, 2011.
The performance of many dynamic language implementations suffers from high allocation rates and runtime type checks. This makes dynamic languages less applicable to purely algorithmic problems, despite their growing popularity. In this paper we present a simple compiler optimization based on online partial evaluation to remove object allocations and runtime type checks in the context of a tracing JIT. We evaluate the optimization using a Python VM and find that it gives good results for all our (real-life) benchmarks.
Requirements, Traceability and DSLs in Eclipse with the Requirements Interchange Format (RIF/ReqIF)
[PDF] [Bibtex]Technical Report, Dagstuhl-Workshop MBEES 2011: Modellbasierte Entwicklung eingebetteter Systeme, 2011.
Requirements engineering (RE) is a crucial aspect in systems development and is the area of ongoing research and process improvement. However, unlike in modelling, there has been no established standard that activities could converge on.
In recent years, the emerging Requirements Interchange Format (RIF/ReqIF) gained more and more visibility in industry, and research projects start to investigate these standards. To avoid redundant efforts in implementing the standard, the VERDE and Deploy projects cooperate to provide a stable common basis for RIF/ReqIF that could be leveraged by other research projects too. In this paper, we present an Eclipse-based extensible implementation of a RIF/ReqIF-based requirements editing platform.
In addition, we are concerned with two related aspects of RE that take advantage of the common platform. First, how can the quality of requirements be improved by replacing or complementing natural language requirements with formal approaches such as domain specific languages or models. Second, how can we establish robust traceability that links requirements and model constructs and other artefacts of the development process. We present two approaches to traceability and two approaches to modelling.
We believe that our research represents a significant contribution to the existing tooling landscape, as it is the first clean-room implementation of the RIF/ReqIF standard. We believe that it will help reduce gaps in often heterogeneous tool chains and inspire new conceptual work and new tools.
2010
Efficient Approximate Verification of B via Symmetry Markers
[PDF] [Bibtex]Annals of Mathematics and Artificial Intelligence, 59(1): 81-106, 2010.
We present a new approximate verification technique for falsifying the invariants of B models. The technique employs symmetry of B models induced by the use of deferred sets. The basic idea is to efficiently compute markers for states, so that symmetric states are guaranteed to have the same marker (but not the other way around).
The falsification algorithm then assumes that two states with the same marker can be considered symmetric. We describe how symmetry markers can be efficiently computed and empirically evaluate an implementation, showing both very good performance results and a high degree of precision (i.e., very few non-symmetric states receive the same marker).
We also identify a class of B models for which the technique is precise and therefore provides an efficient and complete verification method. Finally, we show that the technique can be applied to Z models as well.
Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more
[PDF] [Bibtex]Software Tools for Technology Transfer (STTT), 12(1): 9-21, 2010.
The size of formal models is steadily increasing and there is a demand from industrial users to be able to use expressive temporal query languages for validating and exploring high-level formal specifications. We present an extension of LTL, which is well adapted for validating B, Z and CSP specifications. We present a generic, flexible LTL model checker, implemented inside the ProB tool, that can be applied to a multitude of formalisms such as B, Z, CSP, B CSP, as well as Object Petri nets, compensating CSP, and dSL. Our algorithm can deal with deadlock states, partially explored state spaces, past operators, and can be combined with existing symmetry reduction techniques of ProB. We establish correctness of our algorithm in general, as well as combined with symmetry reduction. Finally, we present various applications and empirical results of our tool, showing that it can be applied successfully in practice.
ProR, an Open Source Platform for Requirements Engineering based on RIF
[PDF] [Bibtex]SEISCONF, 2010.
Proper tool support in requirements engineering is important. A number of proprietary solutions are available in the market place, but few open solutions, and none that are widespread at this time.
In this paper, we introduce ProR, an open platform for requirements engineering. The project was initiated by the EU FP7 Project ``Deploy'', which has the goal to make major advances in engineering methods for dependable systems through the deployment of formal engineering methods. Rather than building a project-specific solution, we decided to develop an extensible, general purpose platform.
We based the tool's data model on the Requirements Interchange Format (RIF / ReqIF), a standard driven by the automotive industry. This gives us interoperability with a number of existing tools. The tool is based on the Eclipse Platform and uses the Eclipse Modeling Framework (EMF). We managed to establish a cooperation with the ITEA-Project ``Verde'', which supplied the implementation of the RIF data model.
In this paper, we will introduce the tool, describe its architecture, and present a small case study. ProR is still under development, and we welcome contributors and are very interested in potential users to validate our approach. Please visit www.pror.org for more information, and to download the current development version.
In ABZ 2010, Lecture Notes in Computer Science, Springer-Verlag, 2010.
Event-B does not provide specific support for the modelling of problems that require some structuring, such as, local variables or sequential ordering of events. All variables need to be declared globally and sequential ordering of events can only be achieved by abstract program counters. This has two unfortunate consequences: such models become less comprehensible - we have to infer sequential ordering from the use of program counters; proof obligation generation does not consider ordering - generating too many proof obligations (although these are usually trivially discharged). In this article we propose a method for specifying structured models avoiding, in particular, the use of abstract program counters. It uses a notation that mainly serves to drive proof obligation generation. However, the notation also describes the structure of a model explicitly. A corresponding graphical notation is introduced that visualises the structure of a model.
In PPDP '10 - Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming, ACM, 2010.
Most Prolog implementations are implemented in low-level languages such as C and are based on a variation of the WAM instruction set, which enhances their performance but makes them hard to write. We present a high-level continuation-based Prolog interpreter written in RPython, a restricted subset of Python. This interpreter is annotated with hints, so that it can be fed through the PyPy tracing JIT generator, which incorporates partial evaluation techniques. The resulting Prolog implementation is surprisingly efficient: it clearly outperforms existing implementations of Prolog in high-level languages such as Java. Moreover, on some benchmarks, our system outperforms state-of-the-art WAM-based Prolog implementations. Our paper tries to show that PyPy can indeed form the basis for implementing programming languages other than Python. Furthermore, we believe that our results showcase the great potential of the tracing JIT approach for declarative programming languages
A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking
[PDF] [Bibtex]In Proceedings ABZ'2010, volume 5977 of Lecture Notes in Computer Science, Springer-Verlag, 2010.
Symmetry reduction is a model checking technique that can help alleviate the problem of state space explosion, by preventing redundant state space exploration. In previous work, we have developed three effective approaches to symmetry reduction for B that have been implemented into the ProB model checker, and we have proved the soundness of our state symmetries. However, it is also important to show our techniques are sound with respect to standard model checking, at the algorithmic level. In this paper, we present a retrospective B development that addresses this issue through a series of B refinements. This work also demonstrates the valuable insights into a system that can be gained through formal modelling.
Refinement-Animation for Event-B - Towards a Method of Validation
[PDF] [Bibtex]In Proceedings ABZ'2010, volume 5977 of Lecture Notes in Computer Science, Springer-Verlag, 2010.
We provide a detailed description of refinement in Event-B, both as a contribution in itself and as a foundation for the approach to simultaneous animation of multiple levels of refinement that we propose. We present an algorithm for simultaneous multi-level animation of refinement, and show how it can be used to detect a variety of errors that occur frequently when using refinement. The algorithm has been implemented in ProB and we applied it to several case studies, showing that multi-level animation is tractable also on larger models.
Fast and Accurate Strong Termination Analysis with an Application to Partial Evaluation
[PDF] [Bibtex]In Proceedings WFLP'2009, LNCS 5979, Springer-Verlag, 2010.
Directed Model Checking for B: An Evaluation and New Techniques
[PDF] [Bibtex]In SBMF'2010, volume 6527 of Lecture Notes in Computer Science, Springer, 2010.
ProB is a model checker for high-level formalisms such as B, Event-B, CSP and Z. ProB uses a mixed depth-first/breadth-first search strategy, and in previous work we have argued that this can perform better in practice than pure depth-first or breadth-first search, as employed by low-level model checkers. In this paper we present a thorough empirical evaluation of this technique, which confirms our conjecture. The experiments were conducted on a wide variety of B and Event-B models, including several industrial case studies. Furthermore, we have extended ProB to be able to perform directed model checking, where each state is associated with a priority computed by a heuristic function. We evaluate various heuristic functions, on a series of problems, and find some interesting candidates for detecting deadlocks and finding specific target states.
An Approach of Requirements Tracing in Formal Refinement
[PDF] [Bibtex]In VSTTE, volume 6217 of Lecture Notes in Computer Science, Springer, 2010.
Formal modeling of computing systems yields models that are intended to be correct with respect to the requirements that have been formalized. The complexity of typical computing systems can be addressed by formal refinement introducing all the necessary details piecemeal. We report on preliminary results that we have obtained for tracing informal natural-language requirements into formal models across refinement levels. The approach uses the WRSPM reference model for requirements modeling, and Event-B for formal modeling and formal refinement. The combined use of WRSPM and Event-B is facilitated by the rudimentary refinement notion of WRSPM, which provides the foundation for tracing requirements to formal refinements.
We assume that requirements are evolving, meaning that we have to cope with frequent changes of the requirements model and the formal model. Our approach is capable of dealing with frequent changes, making use of corresponding techniques already built into the Event-B method.
Proceedings of AVoCS 2010 and Rodin 2010
[Bibtex]2010.
GEPAVAS Gerichtete und parallele Validierung von abstrakten Spezifikationen - Projektreport
[PDF] [Bibtex]Technical Report, University of Düsseldorf, 2010.
2009
On the Purpose of Event-B Proof Obligations
[Bibtex]Formal Aspects of Computing, 2009.
Event-B is a formal modelling method which is claimed to be suitable for diverse modelling domains, such as reactive systems and sequential program development. This claim hinges on the fact that any particular model has an appropriate semantics. In Event-B this semantics is provided implicitly by proof obligations associated with a model. There is no fixed semantics though. In this article we argue that this approach is beneficial to modelling because we can use similar proof obligations across a variety of modelling domains. By way of two examples we show how similar proof obligations are linked to different semantics. A small set of proof obligations is thus suitable for a whole range of modelling problems in diverse modelling domains.
Jean-Raymond Abrial, Michael Butler,
Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, Laurent Voisin
Rodin: An Open Toolset for Modelling and Reasoning in Event-B
[Bibtex]Software Tools for Technology Transfer, 2009.
Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. In this article we present the Rodin modelling tool that seamlessly integrates modelling and proving. We outline how the Event-B language was designed to facilitate proof and how the tool has been designed to support changes to models while minimising the impact of changes on existing proofs. We outline the important features of the prover architecture and explain how well-definedness is treated. The tool is extensible and configurable so that it can be adapted more easily to different application domains and development methods.
Validating and Animating Higher-Order Recursive Functions in B
[PDF] [Bibtex]In Festschrift for Egon Börger, volume 5115 of Lecture Notes in Computer Science, Springer-Verlag, 2009.
ProB is an animation and model checking tool for the B Method, which can deal with many interesting specifications. Some specifications, however, contain complicated functions which cannot be represented explicitly by a tool. We present a scheme with which higher-order recursive functions can be encoded in B, and establish soundness of this scheme. We then describe a symbolic representation for such functions. This representation enables ProB to successfully animate and model check a new class of relevant specifications, where animation is especially important due to the involved nature of the specification.
Tracing the Meta-Level: PyPy's Tracing JIT Compiler
[PDF] [Bibtex]In ICOOOLPS 2009, 2009.
We attempt to apply the technique of Tracing JIT Compilers in the context of the PyPy project, i.e. to programs that are interpreters for some dynamic languages, including Python. Tracing JIT compilers can greatly speed up programs that spend most of their time in loops in which they take similar code paths. However, applying an unmodified tracing JIT to a program that is itself a bytecode interpreter results in very limited or no speedup. In this paper we show how to guide tracing JIT compilers to greatly improve the speed of bytecode interpreters. One crucial point is to unroll the bytecode dispatch loop, based on two hints provided by the implementer of the bytecode interpreter. We evaluate our technique by applying it to two PyPy interpreters: one is a small example, and the other one is the full Python interpreter.
In Logic-Based Program Synthesis and Transformation, 19th International Symposium, LOPSTR 2009, Coimbra, Portugal, September 2009, Revised Selected Papers, volume 6037 of Lecture Notes in Computer Science, Springer, 2009.
We introduce a just-in-time specializer for Prolog. Just-in-time specialization attempts to unify of the concepts and benefits of partial evaluation (PE) and just-in-time (JIT) compilation. It is a variant of PE that occurs purely at runtime, which lazily generates residual code and is constantly driven by runtime feedback. Our prototype is an on-line just-in-time partial evaluator. A major focus of our work is to remove the overhead incurred when executing an interpreter written in Prolog. It improves over classical offline PE by requiring almost no heuristics nor hints from the author of the interpreter; it also avoids most termination issues due to interleaving execution and specialization. We evaluate the performance of our prototype on a small number of benchmarks.
SOC: A Slicer for CSP Specifications
[Bibtex]In PEPM 2009, ACM Press, 2009.
This paper describes SOC, a program slicer for CSP specifications. In order to increase the precision of program slicing, SOC uses a new data structure called Context-sensitive Synchronized Control Flow Graph (CSCFG). Given a CSP specification, SOC generates its associated CSCFG and produces from it two different kinds of slices; which correspond to two different static analyses. We present the tool's architecture, its main applications and the results obtained from experiments conducted in order to measure the performance of the tool.
SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook
[PDF] [Bibtex]In Proceedings AFM 2009, 2009.
ProB is a model checker for high-level B and Event-B models based on constraint-solving. In this paper we investigate alternate approaches for validating high-level B models using alternative techniques and tools based on using BDDs, SAT-solving and SMT-solving. In particular, we examine whether PROB can be complemented or even supplanted by using one of the tools BDDBDDB, Kodkod or SAL.
Automated Property Verification for Large Scale B Models
[PDF] [Bibtex]In Proceedings FM 2009, volume 5850 of Lecture Notes in Computer Science, Springer-Verlag, 2009.
In this paper we describe the successful application of the ProB validation tool on an industrial case study. The case study centres on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for AtelierB. AtelierB, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense (and they need to be revalidated whenever the rail network infrastructure changes).
In this paper we show how we were able to use ProB to validate all of the about 300 properties of the San Juan deployment, detecting exactly the same faults automatically in around 17 minutes that were manually uncovered in about one man-month. This achievement required the extension of the ProB kernel for large sets as well as an improved constraint propagation phase. We also outline some of the effort and features that were required in moving from a tool capable of dealing with medium-sized examples towards a tool able to deal with actual industrial specifications. Notably, a new parser and type checker had to be developed. We also touch upon the issue of validating ProB, so that it can be integrated into the SIL4 development chain at Siemens
In Proceedings SEKE, Knowledge Systems Institute, 2009.
Visualizing graphs with a large number of edges and vertices can be cumbersome and ineffective. This is due to the presence of countless overlapping arrows, which makes a graph unclear and hard to understand and interpret by a human. The aim of this paper is to try to address this problem using a new concept of data visualization, namely pie tree visualization. We illustrate this technique on the module architecture of a real-life development from the project Deploy. We first describe pie tree visualization, and then, present its advantages.
Applying Model Checking to Generate Model-based Integration Tests from Choreography Models
[PDF] [Bibtex]In Proceedings TESTCOM/FATES 2009, volume 5826 of Lecture Notes in Computer Science, Springer-Verlag, 2009.
Choreography models describe the communication protocols between services. Testing of service choreographies is an important task for the quality assurance of service-based systems as used e.g. in the context of service-oriented architectures (SOA). The formal modeling of service choreographies enables a model-based integration testing (MBIT) approach. We present MBIT methods for our service choreography modeling approach called Message Choreography Models (MCM). For the model-based testing of service choreographies, MCMs are translated into Event-B models and used as input for our test generator which uses the model checker ProB.
High-Level versus Low-Level Specifications: Comparing B with Promela and ProB with Spin
[PDF] [Bibtex]In Proceedings TFM-B 2009, APCB, 2009.
During previous teaching and research experience, we have accumulated anecdotal evidence that using a high-level formalism such as B can be much more productive than using a low-level formalism such as Promela. Furthermore, quite surprisingly, it turned out that the use of a high-level model checker such as prob, was much more effective in practice than using a very efficient model checker such as spin on the corresponding low-level model. In this paper, we try to put this anecdotal evidence on a more firm empirical footing, by systematically comparing the development and validation of B models with the development and validation corresponding Promela models. These experiments have confirmed our previous experience, and show the merits of using a high-level specification language such as B, both in a teaching and in a research environment.
In Proceedings of Dagstuhl Seminar on Refinement Based Methods for the Construction of Dependable Systems (09381), 2009.
Event-B and the Rodin tool use a number of simple techniques that make the modelling method around them effective in practical applications. We present two of these techniques, anticipation and witnesses. It is interesting how a couple of very simple techniques are so important for the method to work. Finally we propose a small enhancement of Event-B that would extend the use of witnesses.
In Proceedings of FMICS 2009, volume 5825 of Lecture Notes in Computer Science, Springer, 2009.
B-MotionStudio provides a way to quickly generate domain specific visualisations for a formal model, enabling domain experts and managers to understand and validate the model. We also believe that our tool will be of use when teaching formal methods, both during lectures as a way to motivate students to write their own formal models.
In Proceedings of ICFEM 2009, volume 5885 of Lecture Notes in Computer Science, Springer, 2009.
With the aid of the ProB Plugin, the Rodin Platform provides an integrated environment for editing, proving, animating and model checking Event-B models. This is of considerable benefit to the modeler, as it allows him to switch between the various tools to validate, debug and improve his or her models. The crucial idea of this paper is that the integrated platform also provides benefits to the tool developer, i.e., it allows easy access to information from other tools. Indeed, there has been considerable interest in combining model checking, proving and testing. In previous work we have already shown how a model checker can be used to complement the Event-B proving environment, by acting as a disprover. In this paper we show how the prover can help improve the efficiency of the animator and model checker.
Proving Quicksort correct in Event-B
[Bibtex]In Refine 2009, ENTCS, 2009.
The Event-B method can be used to model all sorts of discrete event systems, among them sequential programs. We have made the experience that the minimalist nature of Event-B is of advantage when it comes to tool support and to using proof as a means to analyse a model. The downside of the minimalism is that when models get more complex the lack of structure in the models can make them cluttered with auxiliary variables. System decomposition will not solve this problem. This can not be reasonably applied to a sequential program. In this article we describe our experiences with using Event-B by way of an example. We show how we verified iterative Quicksort in Event-B and intersperse our observations and criticisms. We use them to formulate some suggestions of how we believe Event-B should evolve in future. Some of the minimalism may have to be abandoned in favour of more clarity of the produced formal models.
In TFM 2009, Lecture Notes in Computer Science, Springer-Verlag, 2009.
Usually we teach formal methods relying for a large part on one kind of reasoning technique about a formal model. For instance, we either use formal proof or we use model-checking. It would appear that it is already hard enough to learn one technique and having to cope with two puts just another burden on the students. This is not our experience. Especially model-checking is easily used to complement formal proof. It only relies on an intuitive operational understanding of a formal model. In this article we show how using model-checking, animation, and formal proof together can be used to improve understanding of formal models. We demonstrate how animation can help finding an explanation for a failing proof. We also demonstrate where animation or model-checking may not help and where proving may not help. For most part use of another tool pays off. Proof obligations present intentionally a static view of a system so that we focus on abstract properties of a model and not on its behaviour. By contrast model-checking provides a more dynamic view based on an operational interpretation. Both views are valuable aids to reasoning about a model.
In TFM-B 2009, University of Nantes, 2009.
When teaching Event-B to beginners, we usually start with models that are already good enough, demonstrating occasionally some standard techniques like ``invariant strengthening''. We show that we got it essentially right but need to make improvements here and there. However, this is not how we really create formal models. To a beginner, getting shown only nearly perfect models is overwhelming. So we should start earlier and show how we usually get models wrong initially. This provides ample opportunity to demonstrate the strengths of formal reasoning (and the weaknesses). The principal strength of formal reasoning lies in its capacity to locate mistakes in a model and to suggest corrections. A beginner should learn how to profit from his mistakes by improving his understanding of the model. A weakness of formal reasoning is that we only find mistakes that we expect, for example, invariant violation or non-termination. Mistakes that do not fall into one of these categories may slip through. In this article we present how a formal model is created by refinement and alteration. The approach employs mathematical methodology for problem solving and a software tool. Both aspects are important. Mathematical methodology provides ways to turn mistakes into improvements. The software tool is necessary to ease the impact of changes on a model and to obtain rapid feed back. We begin with a set of assumptions and requirements, the problem, and set out to solve it, giving a more vivid picture of how formal methods work.
Parallel Model Checking of Event-B Specification with ProB
[Bibtex]Work in Progress Report at PDMC 2009, http://www.pdmc.cz/PDMC09/accepted-papers.shtml, 2009.
Integrated Formal Methods: Proceedings iFM 2009
[Bibtex]2009.
2008
Efficient and Flexible Access Control via Jones-Optimal Logic Program Specialisation
[PDF] [Bibtex]Higher-Order and Symbolic Computation, 21(1-2): 5-35, 2008.
We describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and an access policy specification. For processing access control requests we specialise the meta-program for a given access policy and database by using the Logen partial evaluation system. The resulting specialised control checking program is dependent solely upon dynamic information that can only be known at the time of actual access request evaluation. In addition to describing our approach, we give a number of performance measures for our implementation of an access control checker. In particular, we show that by using our approach we get flexible access control with virtually no overhead, satisfying the Jones optimality criterion. The paper also shows how to satisfy the Jones optimality criterion more generally for interpreters written in the non-ground representation.
La validation de modèles Event-B avec le plug-in ProB pour RODIN
[Bibtex]Technique et Science Informatiques, 27(8): 1065-1084, 2008.
Probing the Depths of CSP-M: A new FDR-compliant Validation Tool
[PDF] [Bibtex]ICFEM 2008, 2008.
We present a new animation and model checking tool for CSP. The tool covers the CSP-M language, as supported by existing tools such as fdr and probe. Compared to those tools, it provides visual feedback in the source code, has an LTL model checker and can be used for combined CSP||B specifications. During the development of the tool some intricate issues were uncovered with the CSP-M language. We discuss those issues, and provide suggestions for improvement. We also explain how we have ensured conformance with fdr, by using fdr itself to validate our tool's output. We also provide empirical evidence on the performance of our tool compared to fdr, showing that it can be used on industrial-strength specifications.
ProB: An Automated Analysis Toolset for the B Method
[PDF] [Bibtex]Software Tools for Technology Transfer (STTT), 10(2): 185-203, 2008.
We present ProB, a validation toolset for the B method. ProB's automated animation facilities allow users to gain confidence in their specifications. ProB also contains a model checker and a refinement checker, both of which can be used to detect various errors in B specifications. We describe the underlying methodology of ProB, and present the important aspects of the implementation. We also present empirical evaluations as well as several case studies, highlighting that ProB enables users to uncover errors that are not easily discovered by existing tools.
A roadmap for the Rodin Toolset
[Bibtex]In ABZ 2008, Lecture Notes in Computer Science, Verlag, 2008.
Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. The continued development of the Rodin toolset is funded by the EU research project ICT 214158 DEPLOY (Industrial deployment of system engineering methods providing high dependability and productivity) www.deploy-project.eu. The toolset was originally developed as part of the project IST 511599 RODIN (Rigorous Open Development Environment for Complex Systems).
In ABZ 2008, Lecture Notes in Computer Science, Springer-Verlag, 2008.
Event-B is a formal modelling method which is claimed to be suitable for diverse modelling domains, such as reactive systems and sequential program development. This claim hinges on the fact that any particular model has an appropriate semantics. In Event-B this semantics is provided implicitly by proof obligations associated with a model. There is no fixed semantics though. In this article we argue that this approach is beneficial to modelling because we can use similar proof obligations across a variety of modelling domains. By way of two examples we show how similar proof obligations are linked to different semantics. A small set of proof obligations is thus suitable for a whole range of modelling problems in diverse modelling domains.
The High Road to Formal Validation: Model Checking High-Level versus Low-Level Specifications
[PDF] [Bibtex]In ABZ 2008, volume 5238 of Lecture Notes in Computer Science, Springer-Verlag, 2008.
In this paper we examine the difference between model checking high-level and low-level models. In particular, we compare the ProB model checker for the B-method and the Spin model checker for Promela. While Spin has a dramatically more efficient model checking engine, we show that in practice the performance can be disappointing compared to model checking high-level specifications with ProB. We investigate the reasons for this behaviour, examining expressivity, granularity and Spin's search algorithms. We also show that certain types of information (such as symmetry) can be more easily inferred and exploited in high-level models, leading to a considerable reduction in model checking time.
In FMCO 2008, Lecture Notes in Computer Science, Springer-Verlag, 2008.
A reasonable approach to formal modelling is to start with a specification that captures the requirements of a system and then use formal refinement to implement it. The problem with this approach is that for complex systems the specification itself is complex. It becomes a challenge to say whether the specification is the right one for the given requirements. Sometimes requirements also concern features of a system closely related to its implementation. This would make an abstract specification necessarily incomplete. We believe that it is better not to follow the rigid approach to modelling described above. Instead, we argue that the specification itself should be elaborated by refinement. Ultimately, the distinction between specification and implementation is no longer made in the strict sense above. There is only one model of the system that is connected by successive refinements. Using Event-B, we demonstrate how this can be applied to cope with the complexity of specifications. On the one hand we benefit from the reduced number of detail to consider at different times. On the other hand we are encouraged to reason about the formal model since the beginning and to rethink it occasionally to capture better its intended behaviour and match the requirements.
In Preproceedings LOPSTR'08, volume 5438 of Lecture Notes in Computer Science, 2008.
This work presents a static slicing based technique to slice CSP specifications. Given a particular event in a CSP specification, our technique allows us to know what parts of the specification must necessarily be executed before this event, and what parts of the specification could be executed before it in some execution. Our technique is based on a new data structure which extends the synchronized CFG. We show that this new data structure improves the synchronized CFG by taking into account the context in which processes are called and, thus, makes the slicing process more precise.
Fast Offline Partial Evaluation for Large Logic Programs
[PDF] [Bibtex]In Proceedings LOPSTR'08, volume 5438 of Lecture Notes in Computer Science, 2008.
In this paper, we present a fast binding-time analysis (BTA) by integrating a size-change analysis, which is independent of a selection rule, into a classical BTA for offline partial evaluation of logic programs. In contrast to previous approaches, the new BTA is conceptually simpler and considerably faster, scaling to medium-sized or even large examples and, moreover, it ensures both the so called local and global termination. We also show that through the use of selective hints, we can achieve both good specialisation results and a fast BTA and specialisation process.
Declarative Programming for Verification: Lessons and Outlook
[PDF] [Bibtex]In Proceedings PPDP'2008, ACM Press, 2008.
This paper summarises roughly ten years of experience using declarative programming for developing tools to validate formal specifications. More precisely, we present insights gained and lessons learned while implementing animators and model checkers in Prolog for various specification languages, ranging from process algebras such as CSP to model-based specifications such as Z and B.
ProB gets Nauty: Effective Symmetry Reduction for B and Z Models
[PDF] [Bibtex]In Proceedings TASE 2008, IEEE, 2008.
Symmetry reduction holds great promise to counter the state explosion problem. However, currently it is ``conducting a life on the fringe'', and is not widely applied, mainly due to the restricted applicability of many of the techniques. In this paper we propose a symmetry reduction technique applied to high-level formal specification languages (B and Z). Not only does symmetry arise naturally in most models, it can also be exploited without restriction by our method. This method translates states of a formal model into directed graphs, and then uses graph canonicalisation to detect symmetries. We use the tool nauty to efficiently perform graph canonicalisation, which we have interfaced with the model checker ProB. In this paper we present the general technique, show how states can be translated first into vertex-coloured graphs suitable for nauty. We present empirical results, showing the effectiveness of our method as well as analysing the cost of graph canonicalisation.
A Semantics-Aware Editing Environment for Prolog in Eclipse
[PDF] [Bibtex]In Proceedings of the 18th Workshop on Logic-based methods in Programming Environments, WLPE, 2008.
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 inte- grated Prolog engine, and can be extended with further semantic analyses, e.g., based on abstract interpretation.
Back to the Future in One Week – Implementing a Smalltalk VM in PyPy
[PDF] [Bibtex]In Self-Sustaining Systems, Lecture Notes in Computer Science, Springer, 2008.
We report on our experiences with the Spy project, including implementation details and benchmark results. Spy is a re-implementation of the Squeak (i.e. Smalltalk-80) VM using the PyPy toolchain. The PyPy project allows code written in RPython, a subset of Python, to be translated to a multitude of different backends and architectures. During the translation, many aspects of the implementation can be independently tuned, such as the garbage collection algorithm or threading implementation. In this way, a whole host of interpreters can be derived from one abstract interpreter definition. Spy aims to bring these benefits to Squeak, allowing for greater portability and, eventually, improved performance. The current Spy codebase is able to run a small set of benchmarks that demonstrate performance superior to many similar Smalltalk VMs, but which still run slower than in Squeak itself. Spy was built from scratch over the course of a week during a joint Squeak-PyPy Sprint in Bern last autumn.
Easy Graphical Animation and Formula Viewing for Teaching B
[PDF] [Bibtex]In The B Method: from Research to Teaching, Lina, 2008.
2007
Debugging Event-B Models using the ProB Disprover Plug-in
[PDF] [Bibtex]Proceedings AFADL'07, 2007.
The B-method, as well as its offspring Event-B, are both tool-supported formal methods used for the development of computer systems whose correctness is formally proven. However, the more complex the specification becomes, the more proof obligations need to be discharged. While many proof obligations can be discharged automatically by recent tools such as the Rodin platform, a considerable number still have to be proven interactively. This can be either because the required proof is too complicated or because the B model is erroneous. In this paper we describe a disprover plugin for Rodin that utilizes the ProB animator and model checker to automatically find counterexamples for a given problematic proof obligation. In case the disprover finds a counterexample, the user can directly investigate the source of the problem (as pinpointed by the counterexample) and should not attempt to prove the proof obligation. We also discuss under which circumstances our plug-in can be used as a prover, i.e., when the absence of a counterexample actually is a proof of the proof obligation.
Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B
[PDF] [Bibtex]Fundamenta Informaticae, 77(1-2): 1-28, 2007.
We argue that formal modeling should be the starting point for any serious development of computer systems. This claim poses a challenge for modeling: at first it must cope with the constraints and scale of serious developments. Only then it is a suitable starting point. We present three techniques, refinement, decomposition, and instantiation, that we consider indispensable for modeling large and complex systems. The vehicle of our presentation is Event-B, but the techniques themselves do not depend on it.
Efficient Approximate Verification of Promela Models via Symmetry Markers
[PDF] [Bibtex]In ATVA, volume 4762 of Lecture Notes in Computer Science, Springer-Verlag, 2007.
We present a new verification technique for Promela which exploits state-space symmetries induced by scalarset values used in a model. The technique involves efficiently computing a marker for each state encountered during search. We propose a complete verification method which only partially exploits symmetry, and an approximate verification method which fully exploits symmetry. We describe how symmetry markers can be efficiently computed and integrated into the Spin tool, and provide an empirical evaluation of our technique using the Topspin symmetry reduction package, which shows very good performance results and a high degree of precision for the approximate method (i.e. very few non-symmetric states receive the same marker). We also identify a class of models for which the approximate technique is precise.
In B 2007, volume 4591 of Lecture Notes in Computer Science, Springer-Verlag, 2007.
Event-B is a notation and method for discrete systems modelling by refinement. The notation has been carefully designed to be simple and easily teachable. The simplicity of the notation takes also into account the support by a modelling tool. This is important because Event-B is intended to be used to create complex models. Without appropriate tool support this would not be possible. This article presents justifications and explanations for the choices that have been made when designing the Event-B notation.
In BCS-FACS Christmas 2007 Meeting, 2007.
We present a software tool, the Rodin tool, for formal modelling in Event-B. Event-B is a notation and method developed from the B-Method and is intended to be used with an incremental style of modelling. The idea of incremental modelling has been taken from programming: modern programming languages come with integrated development environments that make it easy to modify and improve programs. The Rodin tool provides such an environment for Event-B. The two main characteristics of the Rodin tool are its ease of use and its extensibility. The tool focuses on modelling. It is easy to modify models and try out variations of a model. The tool can also be extended easily. This will make it possible to adapt the tool specific needs. So the tool can be adapted to fit into existing development processes instead demanding the opposite. We believe that these two characteristics are major points for industrial uptake.
In IFM 2007, Lecture Notes in Computer Science, Springer-Verlag, 2007.
Event-B is a notation and method for discrete systems modelling by refinement. We introduce a small but very useful construction: qualitative probabilistic choice. It extends the expressiveness of Event-B allowing us to prove properties of systems that could not be formalised in Event-B before. We demonstrate this by means of a small example, part of a larger Event-B development that could not be fully proved before. An important feature of the introduced construction is that it does not complicate the existing Event-B notation or method, and can be explained without referring to the underlying more complicated probabilistic theory. The necessary theory itself is briefly outlined in this article to justify the soundness of the proof obligations given. We also give a short account of alternative constructions that we explored, and rejected.
Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more
[Bibtex]In ISoLA, volume RNTI-SM-1 of Revue des Nouvelles Technologies de l'Information, 2007.
The size of formal models is steadily increasing and there is a demand from industrial users to be able to use expressive temporal query languages for validating and exploring high-level formal specifications. We present an extension of LTL, which is well adapted for validating B, Z and CSP specifications.
We present a generic, flexible LTL model checker, implemented inside the ProB tool, that can be applied to a multitude of formalisms such as B, Z, CSP, B CSP, as well as Object Petri nets, compensating CSP, and dSL. Our algorithm can deal with deadlocking states, partially explored state spaces, past operators, and can be combined with existing symmetry reduction techniques of ProB. We establish correctness of our algorithm in general, as well as combined with symmetry reduction.
Finally, we present various applications and empirical results of our tool, showing that it can be applied successfully in practice.
Validating Z Specifications using the ProB Animator and Model Checker
[PDF] [Bibtex]In Integrated Formal Methods, volume 4591 of Lecture Notes in Computer Science, Springer-Verlag, 2007.
We present the architecture and implementation of the ProZ tool to validate high-level Z specifications. The tool was integrated into ProB, by providing a translation of Z into B and by extending the kernel of ProB to accommodate some new syntax and data types. We describe the challenge of going from the tool friendly formalism B to the more specification-oriented formalism Z, and show how many Z specifications can be systematically translated into B. We describe the extensions, such as record types and free types, that had to be added to the kernel to support a large subset of Z. As a side-effect, we provide a way to animate and model check records in ProB. By incorporating ProZ into ProB, we have inherited many of the recent extensions developed for B, such as the integration with CSP or the animation of recursive functions. Finally, we present a successful industrial application, which makes use of this fact, and where ProZ was able to discover several errors in Z specifications containing higher-order recursive functions.
In Practical Applications of Declarative Languages (PADL'07), Lecture Notes in Computer Science, Springer-Verlag, 2007.
In aspect-oriented programming, pointcuts are usually compiled by identifying a set of shadows - that is, places in the code whose execution is potentially relevant for a pointcut - and inserting dynamic checks at these places for those parts of the pointcut that cannot be evaluated statically. Today, the algorithms for shadow and check computation are specific for every pointcut designator. This makes it very tedious to extend the pointcut language. We propose the use of declarative languages, together with associated analysis and specialisation tools, to implement powerful and extensible pointcut languages. More specifically, we propose to synthesize (rather than program manually) the shadow and dynamic check algorithms. With this approach, it becomes easier to implement powerful pointcut languages efficiently and to keep pointcut languages open for extension.
How to not write Virtual Machines for Dynamic Languages
[PDF] [Bibtex]In Proceeding of Dyla 2007, 2007.
Typical modern dynamic languages have a growing number of implementations. We explore the reasons for this situation, and the limitations it imposes on open source or academic communities that lack the resources to fine-tune and maintain them all. It is sometimes proposed that implementing dynamic languages on top of a standardized general-purpose ob ject-oriented virtual machine (like Java or .NET) would help reduce this burden. We propose a complementary alternative to writing custom virtual machine (VMs) by hand, validated by the PyPy pro ject: flexibly generating VMs from a high-level ?specification?, inserting features and low-level details automatically ? including good just-in-time compilers tuned to the dynamic language at hand. We believe this to be ultimately a better investment of efforts than the development of more and more advanced general-purpose object oriented VMs. In this paper we compare these two approaches in detail.
In Proceedings B'2007, volume 4355 of Lecture Notes in Computer Science, Springer-Verlag, 2007.
Symmetry reduction is an established method for limiting the amount of states that have to be checked during exhaustive model checking. The idea is to only verify a single representative of every class of symmetric states. However, computing this representative can be nontrivial, especially for a language such as B with its involved data structures and operations. In this paper, we propose an alternate approach, called permutation flooding. It works by computing permutations of newly encountered states, and adding them to the state space. This turns out to be relatively unproblematic for B?s data structures and we have implemented the algorithm inside the ProB model checker. Empirical results confirm that this approach is effective in practice; speedups exceed an order of magnitude in some cases. The paper also contains correctness results of permutation flooding, which should also be applicable for classical symmetry reduction in B.
Efficient Approximate Verification of B via Symmetry Markers
[PDF] [Bibtex]In Proceedings International Symmetry Conference, 2007.
In Proceedings TASE 2007, IEEE, 2007.
Symmetry reduction is a technique that can help alleviate the problem of state space explosion in model checking. The idea is to verify only a subset of states from each class (orbit) of symmetric states. This paper presents a framework for symmetry reduced model checking of B machines, which verifies a unique representative from each orbit. Symmetries are induced by the deferred set; a key component of the B language. This contrasts with strategies that require the introduction of a special data type into a language, to indicate symmetry. An extended version of the graph isomorphism program, textitnauty, is used to detect symmetries, and the symmetry reduction package has been integrated into the ProB model checker. Experimental results illustrate the effectiveness of the method, where exponential speedups are sometimes possible. Relevant algorithms are presented, and there is a comparison with an alternate symmetry reduction strategy, called permutation flooding.
In Proceedings of B 2007, volume 4355 of Lecture Notes in Computer Science, Springer, 2007.
Writing a formal specification for real-life, industrial problems is a difficult and error prone task, even for experts in formal methods. In the process of specifying a formal model for later refinement and implementation it is crucial to get approval and feedback from domain experts to avoid the costs of changing a specification at a late point of the development. But understanding formal models written in a specification language like B requires mathematical knowledge a domain expert might not have. In this paper we present a new tool to visualize B Machines using the ProB animator and Macromedia Flash. Our tool offers an easy way for specifiers to build a domain specific visualization that can be used by domain experts to check whether a B specification corresponds to their expectations.
In Proceedings of B 2007, volume 4355 of Lecture Notes in Computer Science, Springer, 2007.
The open-source Eclipse platform has become hugely popular as an integrated development environment for Java, and a considerable number of plug-ins have been developed for other programming languages (e.g., C++,PHP, Eiffel, Python, Fortran, etc.). In this paper we present a new plug-in for Eclipse, supporting the B-method and B's abstract machine notation (AMN). In addition to providing editing and syntax highlighting, the plug-in displays syntax and structural errors in the B source code, as well as suggesting fixes for those errors.
Automatic Testing from Formal Specifications
[Bibtex]In Tests and Proofs (TAP 2007), volume 4454 of Lecture Notes in Computer Science, Springer-Verlag, 2007.
Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more
[PDF] [Bibtex]Technical Report, No. STUPS/2007/02, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, 2007.
This technical report is an extension to the conference paper with the same name. It contains the proofs that were omitted in the conference paper.
2006
Holistic Trust Design of E-Services
[Bibtex]In Ronggong Song, Larry Korba, George Yee (ed.): Trust in E-services: Technologies, Practices and Challenges, IGI Global: 113-139, 2006.
Animating and Model Checking B Specifications with Higher-Order Recursive Functions
[PDF] [Bibtex]In Dagstuhl Seminar 06191 "Rigorous Methods for Software Construction and Analysis", 2006.
An open extensible tool environment for Event-B
[Bibtex]In ICFEM 2006, Lecture Notes in Computer Science, Springer-Verlag, 2006.
We consider modelling indispensable for the development of complex systems. Modelling must be carried out in a formal notation to reason and make meaningful conjectures about a model. But formal modelling of complex systems is a difficult task. Even when theorem provers improve further and get more powerful, modelling will remain difficult. The reason for this that modelling is an exploratory activity that requires ingenuity in order to arrive at a meaningful model. We are aware that automated theorem provers can discharge most of the onerous trivial proof obligations that appear when modelling systems. In this article we present a modelling tool that seamlessly integrates modelling and proving similar to what is offered today in modern integrated development environments for programming. The tool is extensible and configurable so that it can be adapted more easily to different application domains and development methods.
Supervising Offline Partial Evaluation of Logic Programs using Online Techniques
[PDF] [Bibtex]In Proceedings LOPSTR'06, volume 4407 of Lecture Notes in Computer Science, Springer-Verlag, 2006.
The Ecce and Logen Partial Evaluators and their Web Interfaces
[PDF] [Bibtex]In Proceedings PEPM 06, IBM Press, 2006.
We present Ecce and Logen, two partial evaluators for Prolog using the online and offline approach respectively. We briefly present the foundations of these tools and discuss various applications. We also present new implementations of these tools, carried out in Ciao Prolog. In addition to a command-line interface new user-friendly web interfaces were developed. These enable non-expert users to specialise logic programs using a web browser, without the need for a local installation.
2005
Guest Editorial - Special Issue on Automated Verification of Critical Systems
[Bibtex]Formal Aspects of Computing, 17(2): 91-92, 2005.
Rodin Deliverable D10, 2005.
All modelling items used in a formal B development are kept in the database kernel-component. This database is analysed by the static checker with respect to various properties the collection of modelling items must satisfy. When the static checker has accepted the database as being consistent, its items can be submitted to proof obligation generation and subsequent proof. In addition to marking modelling items as consistent the static checker computes auxiliary data structures to improve performance of all tasks that involve using items stored in the database.
ProTest: An Automatic Test Environment for B Specifications
[PDF] [Bibtex]Electronic Notes in Theroretical Computer Science, 111: 113-136, 2005.
We present ProTest, an automatic test environment for B specifications. B is a model-oriented notation where systems are specified in terms of abstract states and operations on abstract states. ProTest first generates a state coverage graph of a B specification through exhaustive model checking, and the coverage graph is traversed to generate a set of test cases, each being a sequence of B operations. For the model checking to be exhaustive, some transformations are applied to the sets used in the B machine. The approach also works if it is not exhaustive; one can stop at any point in time during the state space exploration and generate test cases from the coverage graph obtained so far. ProTest then simultaneously performs animation of the B machine and the execution of the corresponding implementation in Java, and assign verdicts on the test results. With some restrictions imposed on the B operations, the whole of the testing process is performed mechanically. We demonstrate the efficacy of our test environment by performing a small case study from industry. Furthermore, we present a solution to the problem of handling non-determinism in B operations.
Tools for system validation with B abstract machines
[PDF] [Bibtex]In 12th International Workshop on Abstract State Machines, 2005.
In this paper we give an overview of some tools that we have developed to support the application of the B Method. ProB is an animation and model checking tool for the B method. ProB's animation facilities allow users to gain confidence in their specifications. ProB contains a temporal and a state-based model checker, both of which can be used to detect various errors in B specifications. We also overview a recent extension of ProB that supports checking of specifications written in a combination of CSP and B. Finally we describe the UML-B profile and associated U2B tool that allows UML and B to be combined and is intended to make modelling with B more appealing to software engineers.
Forward Slicing by Conjunctive Partial Deduction and Argument Filtering
[PDF] [Bibtex]In ESOP, volume 3444 of Lecture Notes in Computer Science, Springer-Verlag, 2005.
Program slicing is a well-known methodology that aims at identifying the program statements that (potentially) affect the values computed at some point of interest. Within imperative programming, this technique has been successfully applied to debugging, specialization, merging, reuse, maintenance, etc. Due to its declarative nature, adapting the slicing notions and techniques to a logic programming setting is not an easy task. In this work, we define the first, semantics-preserving, forward slicing technique for logic programs. Our approach relies on the application of a conjunctive partial deduction algorithm for a precise propagation of information between calls.
We do not distinguish between static and dynamic slicing since partial deduction can naturally deal with both static and dynamic data. Furthermore, this approach can quite easily be implemented by adding a new code generator on top of existing partial deduction systems. A slicing tool has been implemented in ECCE, where a post-processing transformation to remove redundant arguments has been added. Experiments conducted on a wide variety of programs are encouraging and demonstrate the usefulness of our approach, both as a classical slicing method and as a technique for code size reduction.
Combining CSP and B for Specification and Property Verification
[PDF] [Bibtex]In FM'2005, volume 3582 of Lecture Notes in Computer Science, Springer-Verlag, 2005.
Towards Provably Correct Code Generation via Horn Logical Continuation Semantics
[PDF] [Bibtex]In PADL, volume 3350 of Lecture Notes in Computer Science, Springer-Verlag, 2005.
Provably correct compilation is an important aspect in development of high assurance software systems. In this paper we explore approaches to provably correct code generation based on programming language semantics, particularly Horn logical semantics, and partial evaluation. We show that the definite clause grammar (DCG) notation can be used for specifying both the syntax and semantics of imperative languages. We next show that continuation semantics can also be expressed in the Horn logical framework.
A Reconstruction of the Lloyd-Topor Transformation using Partial Evaluation
[PDF] [Bibtex]In Pre-Proceedings of LOPSTR'05, 2005.
The Lloyd-Topor transformation is a classical transformation that translates extended logic programs with logical connectives and explicit quantifiers into normal logic programs. In this paper we show that this translation can be achieved in a natural way by specialising a meta-interpreter for extended logic programs. For this we use the Logen partial evaluation system, extended to handle coroutining.
In Proceedings ICFEM, volume 3785 of Lecture Notes in Computer Science, Springer-Verlag, 2005.
Self-Tuning Resource Aware Specialisation for Prolog
[PDF] [Bibtex]In Proceedings PPDP'2005, ACM Press, 2005.
The paper develops a self-tuning resource aware partial evaluation technique for Prolog programs, which derives its own control strategies tuned for the underlying computer architecture and Prolog compiler using a genetic algorithm approach. The algorithm is based on mutating the annotations of offline partial evaluation.
Using a set of representative sample queries it decides upon the fitness of annotations, controlling the trade-off between code explosion, speedup gained and specialisation time. The user can specify the importance of each of these factors in determining the quality of the produced code, tailoring the specialisation to the particular problem at hand.
We present experimental results for our implemented technique on a series of benchmarks. The results are compared against the aggressive termination based binding-time analysis and optimised using different measures for the quality of code. We also show that our technique avoids some classical pitfalls of partial evaluation.
A Trust Analysis Methodology for Pervasive Computing Systems
[PDF] [Bibtex]In Trusting Agents for trusting Electronic Societies, volume 3577 of Lecture Notes in Computer Science, Springer-Verlag, 2005.
We present an analysis Trust Analysis Methodology for finding trust issues within pervasive computing systems. It is based on a systematic analysis of scenarios that describe the typical use of the pervasive system by using a Trust Analysis Grid. The Trust Analysis Grid is composed of eleven Trust Issue Categories that cover the various aspects of the concept of trust in pervasive computing systems. The Trust Analysis Grid is then used to guide the design of the pervasive computing system.
In ZB, volume 3455 of Lecture Notes in Computer Science, Springer-Verlag, 2005.
ProB is an animator and model checker for the B method. It also allows to visualise the state space of a B machine in graphical way. This is often very useful and allows users to quickly spot whether the machine behaves as expected. However, for larger state spaces the visualisation quickly becomes difficult to grasp by users (and the computation of the graph layout takes considerable time). In this paper we present two relatively simple algorithms to often considerably reduce the complexity of the graphs, while still keeping relevant information. This makes it possible to visualise much larger state spaces and gives the user immediate feedback about the overall behaviour of a machine. The algorithms have been implemented within the ProB toolset and we highlight their potential on several examples. We also conduct a thorough experimentation of the algorithm on 47 B machines and analyse the results.
Technical Report, Information Security, ETH Zürich, 2005.
This text describes a proof obligation generator for EventB. Most of the document describes the actual generated proof obligations and justification of their correctness. The algorithm for their generation is very simple. We distinguish generated proof obligations from theoretical ones. Theoretical proof obligations are well-suited for hand-written mathematical proofs but less suited for machine-assisted proof. In particular, generated proof obligations have be obtained by decomposing theoretical proof obligations as far as possible so that they are as simple as possible; and hopefully provable by an automatic prover. Substitutions produced by the proof obligation generator are left unevaluated. These are applied in a preprocessing step of the proof manager. The reason for this is to keep the design of the proof obligation generator distinct from the actual provers. By using witnesses in models a part of the proof has been moved into modelling itself. The price to pay is that one has to think about proving while modelling. The advantage is that proofs are decomposed and almost all existential quantifiers are removed from the consequents of proof obligations. There are three main sections on contexts, initial models, and refined models. Each of these contains three subsections: the description subsection introduces the notation used in the section; the theory subsection presents the theoretical proof obligations and derives the generated proof obligations by proof; the generated proof obligations subsection contains the list of proof obligations to be generated by the proof obligation generator. This last section also contains proof obligations for well-definedness. On first reading well-definedness proof obligations should be ignored. These are necessary but are actually not derived from the theoretical proof obligations.
2004
A Framework for the Integration of Partial Evaluation and Abstract Interpretation of Logic Programs
[PDF] [Bibtex]ACM Transactions on Programming Languages and Systems (TOPLAS), 26(3): 413-463, 2004.
Recently the relationship between abstract interpretation and program specialization has received a lot of scrutiny, and the need has been identified to extend program specialization techniques so to make use of more refined abstract domains and operators. This paper clarifies this relationship in the context of logic programming, by expressing program specialization in terms of abstract interpretation. Based on this, a novel specialization framework, along with generic correctness results for computed answers and finite failure under SLD-resolution, is developed.
This framework can be used to extend existing logic program specialization methods, such as partial deduction and conjunctive partial deduction, to make use of more refined abstract domains. It is also shown how this opens up the way for new optimizations. Finally, as shown in the paper, the framework also enables one to prove correctness of new or existing specialization techniques in a simpler manner.
The framework has already been applied in the literature to develop and prove correct specialization algorithms using regular types, which in turn have been applied to the verification of infinite state process algebras.
Construction sûre de systèmes électroniques
[Bibtex]Génie Logiciel(67): 38-44, 2004.
Le développement de systèmes à l'aide du raffinement est une méthode formelle qui permet de gérer la complexité d'un système et de sa preuve de correction en permettant l'introduction des détails du système pas à pas. A partir d'un système abstrait, chaque pas de raffinement est prouvé correct jusqu'au niveau d'implantation. La méthode B est basée sur le raffinement, mais elle aide aussi à gérer les obligations de preuve qui se présentent à chaque pas. La méthode B est l'une des méthodes qui possdent le plus d'outils support pour être utilisée en pratique. Les systèmes électroniques deviennent de plus en plus complexes, l'approche traditionnelle qui consiste à garantir la correction par la simulation ne suffit plus. Par ailleurs, les systèmes électroniques sont de plus en plus présents dans les systmes de toute nature et l'exigence en qualité est de plus en plus forte. Les méthodes formelles sont les seules à pouvoir faire face à cette complexité croissante. Nous présentons dans cet article comment la méthode B peut être utilisée pour la conception des systèmes électroniques.
Embedded System Design Using Formal Model Refinement: An Approach Based on the Combined Use of UML and the B Language
[Bibtex]Design Automation for Embedded Systems, 9(2): 67-99, 2004.
The approach proposed in this paper introduces a hardware/software co-design framework for developing complex embedded systems. The method relies on formal proof of system properties at every phase of the co-design cycle. The key concept is the combined use of UML and the B language for system modeling and design, and the seamless transition from UML specifications to system descriptions in B. The final system prototype emerges from correct-by-construction subsystems described in the B language; the hardware components are translated in VHDL/SystemC, while for the software components C/C++ is used. The outcome is a formally proven correct system implementation. The efficiency of the proposed method is exhibited through the design of a case study from the telecommunication domain.
Offline Specialisation in Prolog Using a Hand-Written Compiler Generator
[PDF] [Bibtex]TPLP, 4(1-2): 139-191, 2004.
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 (called partial deduction when applied to pure logic programs) 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, its specialisation strategy 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. In mixline specialisation some unfolding decisions depend on the outcome of tests performed at specialisation time instead of being hardwired into the specialiser.
Performance analysis of probabilistic action systems
[Bibtex]Formal Aspects of Computing, 16(4): 313-331, 2004.
Formal notations like B or action systems support a notion of refinement. Refinement relates an abstract specification AA to a more deterministic concrete specification CC. Knowing AA and CC one proves CC refines, or implements, specification AA. In this study we consider specification AA as given and concern ourselves with a way to find a good candidate for implementation CC. To this end we classify all implementations of an abstract specification according to their performance. We distinguish performance from correctness. Concrete systems that do not meet the abstract specification correctly are excluded. Only the remaining correct implementations CC are considered with respect to their performance. A good implementation of a specification is identified by having some optimal behaviour in common with it. In other words, a good refinement corresponds to a reduction of non-optimal behaviour. This also means that the abstract specification sets a boundary for the performance of any implementation. We introduce the probabilistic action system formalism which combines refinement with performance. In our current study we measure performance in terms of long-run expected average-cost. Performance is expressed by means of probability and expected costs. Probability is needed to express uncertainty present in physical environments. Expected costs express physical or abstract quantities that describe a system. They encode the performance objective. The behaviour of probabilistic action systems is described by traces of expected costs. A corresponding notion of refinement and simulation-based proof rules are introduced. Probabilistic action systems are based on discrete-time Markov decision processes. Numerical methods solving the optimisation problems posed by Markov decision processes are well-known, and used in a software tool that we have developed. The tool computes an optimal behaviour of a specification AA thus assisting in the search for a good implementation CC.
In J. Mermet (ed.): UML-B Specification for Proven Embedded Systems Design, Kluwer: 109-120, 2004.
In this chapter we discuss modeling of hardware and translation to VHDL. Translation to SystemC or Verilog is similar. However VHDL is easier to read and we use VHDL synthesis tools. Translation is important to provide a complete path from formal models to a circuit. Equally important we need a refinement method to arrive at a formal circuit description that can be translated. This method has some significant differences to the refinement method for software. As one would expect, they are virtually not present at system level but become more and more visible as an actual implementation is approached. This means that the initial refinement steps used in hardware are, in principle, also applicable to software, and vice versa. The subset of the B-language that serves to describe hardware is called BHDL. The definition of the BHDL subset is oriented at the register transfer level for hardware description.
Embedded System Design Using the PUSSEE Method
[Bibtex]In J. Mermet (ed.): UML-B Specification for Proven Embedded Systems Design, Kluwer: 37-52, 2004.
The approach presented in this book relies on the unification of system specification environments for developing electronic systems that are formally proven to be correct (correct-by-construction systems). The key concept conveyed is the formal proof of system properties, which is carried out at every phase of the co-design cycle. The main idea is to build fully functional system models that are formally proven to be correct, and based on them to produce automatically the hardware and the software parts of the system. The approach presented relies on the combined use of UML and B language.
Formal Modelling of Electronic Circuits Using Event-B, Case Study: SAE J1708 Serial Communication Link
[Bibtex]In J. Mermet (ed.): UML-B Specification for Proven Embedded Systems Design, Kluwer: 211-226, 2004.
This chapter presents a study of the SAE J1708 Serial Communication link. The study is carried out in Event-B, an extension of the B method. The system is implemented and decomposed using step-wise refinement. We present how to derive with this method a cycle-accurate hardware model. The model of the communication link system is composed of an arbitrary finite number of identical components that run concurrently. The model contains synchronisation of these components required to control access to the communication link. At the end of the refinement we obtain an implementable model of the components which is translated into VHDL. The generated VHDL design is synthesizable, meaning that the implementable B model is synthesizable as well.
UML-B Specification and Hardware Implementation of a Hamming Coder/Decoder
[Bibtex]In J. Mermet (ed.): UML-B Specification for Proven Embedded Systems Design, Kluwer: 261-278, 2004.
Formal refinement as offered by the B method has been shown to be applicable in practice and to scale up. However, it has been recognised that it is difficult communicate a formal B model with customers. Recently, the UML has been investigated as an interface to rigorous formal B models to facilitate this communication. The UML is generally accepted as being a good vehicle for communicating models of systems. Availability of this interface to the B method addresses a major problem faced by most formal methods: How to validate a formal model with a customer who is not formal methods expert? In this chapter we present an approach to the development of a formally verified circuit implementing a Hamming encoder/decoder. The UML-B is used as a formal specification language and the B method is used to prove refinements until the implementation level at which we can translate into VHDL.
Lix: An Effective Self-applicable Partial Evaluator for Prolog
[PDF] [Bibtex]In FLOPS, Springer-Verlag, 2004.
This paper presents a self-applicable partial evaluator for a considerable subset of full Prolog. The partial evaluator is shown to achieve non-trivial specialisation and be effectively self-applied. The attempts to self-apply partial evaluators for logic programs have, of yet, not been all that successful. Compared to earlier attempts, our LIX system is practically usable in terms of efficiency and can handle natural logic programming examples with partially static data structures, built-ins, side-effects, and some higher-order and meta-level features such as call and findall.
The LIX system is derived from the development of the LOGEN compiler generator system. It achieves a similar kind of efficiency and specialisation, but can be used for other applications. Notably, we show first attempts at using the system for deforestation and tupling in an offline fashion. We will demonstrate that, contrary to earlier beliefs, declarativeness and the use of the ground representation is not the best way to achieve self-applicable partial evaluators.
ProB: Un outil de modélisation formelle (Invited Talk)
[PDF] [Bibtex]In JFPLC, Hermes Science Publications, Lavoisier, 2004.
The development of formal models is often a key step when developing safety or mission critical software. In this setting it is vital to formally check and validate these formal models before translating them into code. I will present ProB, a toolset for the B method which was developed using constraint logic programming technology. ProB allows fully automatic animation of B models, and can be used to systematically check a B model for errors. ProB supports B features such as non-deterministic operations, ANY statements, operations with complex arguments, sets, sequences, functions, lambda abstractions, set comprehensions, constants and properties, and many more. ProB's animation facilities allow users to gain confidence in their specifications, and unlike other animators, the user does not have to guess the right values for the operation arguments or choice variables. This is achieved by using co-routining and finite domain constraint solving. On top of the animation features, ProB contains a temporal model checker and a constraint-based model checker, both of which can be used to detect various errors in B specifications.
In LOPSTR, volume 3573 of Lecture Notes in Computer Science, Springer-Verlag, 2004.
Offline partial evaluation techniques rely on an annotated version of the source program to control the specialisation process. These annotations guide the specialisation and have to ensure termination of the partial evaluation. We present an algorithm for generating these annotations automatically. The algorithm uses state-of-the-art termination analysis techniques, combined with a new type-based abstract interpretation for propagating the binding types. This algorithm has been implemented as part of the Logen partial evaluation system, and we report on performance of the algorithm on a series of benchmarks.
Efficient and Flexible Access Control via Logic Program Specialisation
[PDF] [Bibtex]In PEPM, ACM Press, 2004.
We describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and an access policy specification. We then proceed to specialise the meta-program for a given access policy and intensional database by using the Logen partial evaluation system. In addition to describing the programs involved in our approach, we give a number of performance measures for our implementation of an access control checker, and we discuss the implications of using this approach for access control on deductive databases. In particular, we show that by using our approach we get flexible access control with virtually zero overhead.
In PPDP, ACM Press, 2004.
Object Petri nets (OPNs) provide a natural and modular method for the modelling of many real-world systems. We give a structure-preserving translation of OPNs to Prolog, avoiding the need for an unfolding to a flat Petri net. The translation provides support for reference and value semantics, and even allows different objects to be treated as copyable or non-copyable, respectively. The method is developed for OPNs with arbitrary nesting.
We then apply logic programming tools to animate, compile and model check OPNs. In particular, we use the partial evaluation system LOGEN to produce an OPN compiler, and we use the model checker XTL to verify CTL formulas. We also use LOGEN to produce special purpose model checkers.
We present two case studies, along with experimental results. A comparison to OPN translations to MAUDE specifications and model checking is given, showing that our approach is roughly twice as fast for larger systems. We also tackle infinite state model checking using the ECCE system.
Circuit Design by Refinement in Event-B
[Bibtex]In Proceedings of the Forum on Specification and Design Languages (FDL'04), 2004.
We present the design of a parallel synchronous hardware component from a purely functional description of its behaviour. Starting from an abstract specification of a linear time-invariant (LTI) system in Event-B a pipelined implementation is developed. The presented approach is applicable to LTI systems that can be represented as linear constant-coefficient difference equations. Scheduling and allocation can be conveniently expressed in the Event-B formalism.
In Program Development in Computational Logic, volume 3049 of Lecture Notes in Computer Science, Springer-Verlag, 2004.
Specializing Interpreters using Offline Partial Deduction
[PDF] [Bibtex]In Program Development in Computational Logic, volume 3049 of Lecture Notes in Computer Science, Springer-Verlag, 2004.
We present the latest version of the Logen partial evaluation system for logic programs. In particular we present new binding-types, and show how they can be used to effectively specialise a wide variety of interpreters.We show how to achieve Jones-optimality in a systematic way for several interpreters. Finally, we present and specialise a non-trivial interpreter for a small functional programming language. Experimental results are also presented, highlighting that the Logen system can be a good basis for generating compilers for high-level languages.
The Use of Formal Methods in the Analysis of Trust (Position Paper)
[Bibtex]In iTrust, volume 2995 of Lecture Notes in Computer Science, Springer-Verlag, 2004.
Security and trust are two properties of modern computing systems that are thefocus of much recent interest. They play an increasingly significant role in the requirements for modern computing systems. Security has been studied thoroughly for many years, particularly the sub-domain of cryptography. The use of computing science formal methods has facilitated cryptanalysis of security protocols. At the moment, trust is intensively studied, but not well understood. Here we present our approach based on formal methods for modelling and validating the notion of trust in computing science.
Stephane Lo Presti, Michael Butler,
Michael Leuschel, Colin Snook, Phillip Turner
Formal Modelling and Verification of Trust in a Pervasive Application
[PDF] [Bibtex]Technical Report, DSSE, University of Southampton, 2004.
This report is deliverable WP4-01 of the project ??Trusted Software Agents and Services for Pervasive Information Environments.? The deliverable reports on the activities of formal modelling and verification of a pervasive application which follows from previous results in the project.
The pervasive application is based on several pervasive scenarios already devised and is centred on the user location. This location-based system is first architecturally simplified, while trust requirements are derived from the Trust Analysis Framework presented in the deliverable WP2-01.
This first abstraction is then completed by formal modelling of the system in the B formal method. These models enable us to clarify the decision decisions leading to fulfil the trust requirements. We show that the system policy structure is influenced by the priorities given to the system operations and that a sufficiently high level of abstraction is required to model trust properties.
The modelling activity is completed by formal verification using the ProB model-checker to automate part of this process. Several models are checked successfully, while detection of errors in other models enables us to understand better the behaviour of the system. In particular, issues relative to the dynamicity of modelled elements are highlighted.
The overall methodology followed during these activities proved useful at helping us specifying accurately the trust requirements, so that the pervasive application can be completed in consequence, and is as follows:
1) Model important features of the system First vaguely type the variables; then write a set of operations corresponding to complementary features while (possibly) modifying the variable types to ease this writing; consider the variables by group of similar dynamic properties;
2a) Model-check the model
2a.a) Property violation detected Examine the various aspects of the model (variables, enabled operations, history of operations) to see what part of the property is ??false?; Correct the model accordingly;
2a.b) No property violation detected Go back to 2a until coverage rate is enough; possible changes to the model include: modify the initialisation to test other situations (in B use ??choice by predicate?); add inconsistencies in the model;
2b) Animate the model
2b.a) Execute the desired sequence of operations (validation);
2b.b) Find an interesting state, then 2a.a or 2a.b applies;
2b.c) Backtrack from a state where the invariant is violated;
3) Go back to 1 (complete the model) or refine the model.
Visualising Larger State Spaces in ProB
[Bibtex]Technical Report, ECS, University of Southampton, 2004.
ProB is an animator and model checker for the B method. It also allows to visualise the state space of a B machine in graphical way. This is often very useful and allows users to quickly spot whether the machine behaves as expected. However, for larger state spaces the visualisation quickly becomes difficult to grasp by users (and the computation of the graph layout takes considerable time). In this paper we present two relatively simple algorithms to often considerably reduce the complexity of the graphs, while still keeping relevant information. This makes it possible to visualise much larger state spaces and gives the user immediate feedback about the overall behaviour of a machine. The algorithms have been implemented within the ProB toolset and we highlight their potential on several examples. We also conduct a thorough experimentation of the algorithm on 47 B machines and analyse the results.
2003
Specification and Refinement of Hardware Components in B
[Bibtex]System Specification & Design Languages - Best of FDL '02: 315-325, 2003.
We use the B formalism to derive functionally correct synchronous circuits. To represent the circuit we employ the hardware description language VHDL. This article outlines the development of a circuit design starting from an initial abstract functional specification of a system component. We discuss some topics involved in the translation to synthesisable VHDL and demonstrate the approach by way of an example.
Michael Butler,
Michael Leuschel, Stephane Lo Presti, David Allsopp, Patrick Beautement, Chris Booth, Mark Cusack, Mike Kirton
Towards a Trust Analysis Framework for Pervasive Computing Scenarios
[PDF] [Bibtex]IEEE Computing, 2(3), 2003.
We present a scheme for highlighting the trust issues of merit within pervasive computing, based on an analysis of scenarios from the healthcare domain. The first scenario helps us define an analysis grid, where the human and technical aspects of trust are considered. The analysis is applied to a second scenario to examine its suitability. We then discuss the various categories of the analysis grid in the light of this examination and of the literature on the subject of trust. We believe that this approach could form the basis of a generalised trust analysis framework to support the design, procurement and use of pervasive computing. (The PDF is an extended version of the paper.)
Using the Extensible Model Checker XTL to Verify StAC Business Specifications
[PDF] [Bibtex]In AVoCS, 2003.
Juan Carlos Augusto, Carla Ferreira, Andy M. Gravell,
Michael Leuschel, Karen M.Y. Ng
The Benefits of Rapid Modelling for E-Business System Development
[PDF] [Bibtex]In ER (Workshops), volume 2814 of Lecture Notes in Computer Science, Springer Verlag, 2003.
A Compiler Generator for Constraint Logic Programs
[PDF] [Bibtex]In Ershov Memorial Conference, volume 2890 of Lecture Notes in Computer Science, Springer-Verlag, 2003.
The Cogen approach to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success. This paper demonstrates that the Cogen approach is also applicable to the specialisation of constraint logic programs and leads to effective specialisers. We present the basic specialisation technique for CLP(Q) programs and show how we can handle non-declarative features as well. We present an implemented system along with experimental results.
In FME, volume 2805 of Lecture Notes in Computer Science, Springer-Verlag, 2003.
We present ProB, an animation and model checking tool for the B method. ProB's animation facilities allow users to gain confidence in their specifications, and unlike the animator provided by the B-Toolkit, the user does not have to guess the right values for the operation arguments or choice variables. ProB contains a model checker and a constraint-based checker, both of which can be used to detect various errors in B specifications. We present our first experiences in using ProB on several case studies, highlighting that ProB enables users to uncover errors that are not easily discovered by existing tools.
In GPCE, Lecture Notes in Computer Science, Springer-Verlag, 2003.
We describe the problems associated with the creation of high performance code for mathematical computations. We discuss the advantages and disadvantages of using a high level language like MATLAB and then propose partial evaluation as a way of lessening the disadvantages at little cost. We then go on to describe the design of a partial evaluator for MATLAB and present results showing what performance increases can be achieved and the circumstances in which partial evaluation can provide these.
Inductive Theorem Proving by Program Specialisation: Generating proofs for Isabelle using Ecce (Invited talk)
[PDF] [Bibtex]In LOPSTR, volume 3018 of Lecture Notes in Computer Science, Springer-Verlag, 2003.
In this paper we discuss the similarities between program specialisation and inductive theorem proving, and then show how program specialisation can be used to perform inductive theorem proving. We then study this relationship in more detail for a particular class of problems (verifying infinite state Petri nets) in order to establish a clear link between program specialisation and inductive theorem proving. In particular, we use the program specialiser Ecce to generate specifications, hypotheses and proof scripts in the theory format of the proof assistant Isabelle. Then, in many cases, Isabelle can automatically execute these proof scripts and thereby verify the soundness of Ecce's verification process and of the correspondence between program specialisation and inductive theorem proving.
Improving Compositional Verification of State-based Models by Reducing Modular Unbalance
[PDF] [Bibtex]In Refinement of Critical Systems, 2003.
Compositional Verification is a viable way to tackle the state explosion problem. However, the decomposition of a system into smaller parts is not a trivial problem, and dividing the specification into modules can be regarded as one of the main issues that concerns a compositional approach. This paper concentrates on the application of compositional verification to state-based models, in order to reduce the number of nodes assigned to memory, thus avoiding state explosion and speeding up the verification. Furthermore, we investigate and propose an estimation method that improves the compositional verification process in modular designs, such that the amount of memory required by the process is minimised. This method has been applied to a real-life embedded system, producing meaningful results without the need of data abstraction.
In ZB 2003, Springer-Verlag, 2003.
We present the design of a parallel synchronous hardware component from a purely functional description of its behaviour. Starting from an abstract specification of a linear time-invariant (LTI) system in Event-B a pipelined implementation is developed. The presented approach is applicable to LTI systems that can be represented as linear constant-coefficient difference equations.
Proceedings of the 2003 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'03)
[Bibtex]2003.
This volume contains the papers presented at PEPM'03, the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation. PEPM'03 was held June 7th 2003 in San Diego, California in conjunction with the Programming Language Design and Implementation conference PLDI'03 as part of the Federated Computing Research Conference FCRC 2003. Due to organizational constraints, PEPM'03 had to be held on a single day, restricting the number of talks that could be presented.Papers were judged on their appropriateness for the workshop, their originality, technical strength and clarity. One submission was deemed outside the scope of PEPM, and all the other submissions were reviewed by at least 3 referees, with some help from the following outside reviewers: Elvira Albert, Stephen Craig, Santiago Escobar, and Carla Piazza. The PC meeting was electronic and resulted in 8 submissions being judged of conference quality' and selected for presentation at the workshop and inclusion in the proceedings.
Proceedings of the 3rd Workshop on Automated Verification of Critical Systems (AVoCS'03)
[Bibtex]2003.
The aim of this workshop is to foster a research community in verification in and beyond the United Kingdom of Great Britain through encouraging communication among researchers. Specific objectives include efforts at integration as well as the transfer of methods between different groups from academia and industry. The topics are to be interpreted broadly and inclusively, and in particular cover all aspects of verification (model checking, theorem proving, specification and refinement proofs, etc) pertaining to various types of critical systems, be it safety-critical, business-critical, or performance-critical.
The first meeting, AVoCS'01, was held in Oxford (UK), continuing in the tradition of the annual DERA/OUCL series. The second meeting, AVoCS'02, was held in Birmingham (UK).
Similarly to previous years, the meeting will be informal, and will combine invited lectures with accepted submissions. This year we also want to aim for wider, European and international attention.
Available online at: http://www.ecs.soton.ac.uk/~mal/avocs03/
Specializing Interpreters using Offline Partial Deduction
[PDF] [Bibtex]Technical Report, No. DSSE-TR-2003-5, ECS, University of Southampton, 2003.
We present the latest version of the logen partial evaluation system for logic programs. In particular we present new binding-types, and show how they can be used to effectively specialise a wide variety of interpreters.We show how to achieve Jones-optimality in a systematic way for several interpreters. Finally, we present and specialise a non-trivial interpreter for a small functional programming language. Experimental results are also presented, highlighting that the logen system can be a good basis for generating compilers for high-level languages.
2002
Logic program specialisation through partial deduction: Control Issues
[PDF] [Bibtex]Theory and Practice of Logic Programming, 2(4-5): 461-515, 2002.
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 developing 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.
Finite and Infinite Model Checking of Dual Transition Petri Net Models
[PDF] [Bibtex]In AVoCS, 2002.
Logic programming and partial deduction for the verification of reactive systems: An experimental evaluation
[PDF] [Bibtex]In AVoCS, University of Birmingham, 2002.
In earlier work it has been shown that finite state CTL model checking of reactive systems can be achieved by a relatively simple interpreter written in tabled logic programming.
This approach is flexible in the sense that various specification formalisms can be easily targeted (e.g., Petri nets, CSP, ...). Moreover, infinite state CTL model checking can be performed by analysing this interpreter using a combination of partial deduction and abstract interpretation. It has also been shown that this approach is powerful enough to decide coverability properties of various kinds of Petri nets.
In this ongoing work, we are empirically evaluating these approaches on various case studies of finite, parameterised and infinite systems. For finite state systems, we show how our approach and tool compares to standard tools for finite state model checking For parameterised or infinite state model checking, we are comparing our results with, e.g., XMC, Hytech.
Abstract Conjunctive Partial Deduction using Regular Types and its Application to Model Checking
[Bibtex]In LOPSTR, volume 2372 of Lecture Notes in Computer Science, Springer-Verlag, 2002.
We present an abstract partial deduction technique which uses regular types as its domain and which can handle conjunctions, and thus perform deforestation and tupling. We provide a detailed description of all the required operations and present an implementation within the Ecce system. We discuss the power of this new specialisation algorithm, especially in the light of verifying and specialising infinite state process algebras. Here, our new algorithm can provide a more precise treatment of synchronisation and can be used for refinement checking. Paper Available: http://link.springer.de/link/service/series/0558/tocs/t2372.htm#toc2372
In RCS '02: International Workshop on Refinement of Critical Systems: Methods, Tools and Experience, 2002.
Stepwise refinement transforms an abstract specification into a more deterministic concrete specification. Ultimately one arrives at a specification that is implementable. At the various stages in the refinement process decisions are made that determine how the final implementation operates. Different implementations can be compared with respect to their expected performance within their environment. In this sense refinement poses an optimisation problem. We present a B-based language and a tool that can assist in solving this optimisation problem.
Homeomorphic Embedding for Online Termination of Symbolic Methods
[PDF] [Bibtex]In The Essence of Computation - Essays dedicated to Neil Jones, volume 2566 of Lecture Notes in Computer Science, Springer-Verlag, 2002.
Well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure the termination of techniques for program analysis, specialisation, transformation, and verification. In this paper we survey and discuss this use of homeomorphic embedding and clarify the advantages of such an approach over one using well-founded orders. We also discuss various extensions of the homeomorphic embedding relation. We conclude with a study of homeomorphic embedding in the context of metaprogramming, presenting some new (positive and negative) results and open problems.
Logic Based Program Synthesis and Transformation, Proceedings of LOPSTR'02, Revised Selected Papers
[Bibtex]2002.
Proceedings of the ACM Sigplan International Workshop on Verification and Computational Logic (VCL'2002)
[Bibtex]2002.
Generating inductive verification proofs for Isabelle using the partial evaluator Ecce
[Bibtex]Technical Report, No. DSSE-TR-2002-02, ECS, University of Southampton, 2002.
Ecce is a partial deduction system which can be used to automatically generate abstractions for the model checking of many infinite state systems. We show that to verify the abstractions generated by Ecce we may employ the proof assistant Isabelle. Thereby Ecce is used to generate the specification, hypotheses and proof script in Isabelle's theory format. Then, in many cases, Isabelle can automatically execute these proof scripts and thereby verify the soundness of Ecce's abstraction. In this work we focus on the specification and verification of Petri nets.
2001
Encyclopaedia of Microcomputers, 27: 79-102, 2001.
Temporal Logic Model Checking of CSP: Tools and Techniques
[Bibtex]In AVoCS 2001, Oxford University Computing Laboratory, 2001.
We study the possibility of doing LTL model checking on CSP specifications in the context of refinement. We present a technique to perform LTL model checking of CSP processes using refinement checking in general and the FDR tool in particular. We present a tool which automates the translation process from LTL model checking to CSP refinement. Also, if time permits, we will present another tool which uses latest generation Prolog technology to symbolically animate, compile, and model check CSP specifications.
Design and Implementation of the High-Level Specification Language CSP(LP)
[PDF] [Bibtex]In PADL, volume 1990 of Lecture Notes in Computer Science, Springer, 2001.
We describe practical experiences of using a logic programming based approach to model and reason about concurrent systems. We argue that logic programming is a good foundation for developing, prototyping, animating new specification languages. In particular, we present the new high-level specification language CSP(LP), unifying CSP with concurrent (constraint) logic programming, and which can be used to formally reason both about logical and concurrent aspects of critical systems.
How to make FDR Spin: LTL model checking of CSP using Refinement
[PDF] [Bibtex]In Proceedings FME'2001, Springer-Verlag, 2001.
We study the possibility of doing LTL model checking on CSP specifications in the context of refinement. We present evidence that the refinement-based approach to verification does not seem to be very well suited for verifying certain temporal properties. To remedy this problem, we show how to (and how not to) perform LTL model checking of CSP processes using refinement checking in general and the FDR tool in particular. We show how one can handle (potentially) deadlocking systems, discuss the validity of our approach for infinite state systems, and shed light on the relationship between ``classical'' model checking and refinement checking.
Strategy for Improving Memory Locality Reuse and Exploiting Hidden Parallelism
[Bibtex]In Proceedings of ISSM, 2001.
In recent years, methods for analyzing and parallelizing sequential code using data analysis and loop transformations have been developed. These techniques have proved remarkably successful, and have been used to move from sequential to parallel codes, or to improve efficiency of existing parallel codes. Our research focuses on Fortran code optimisation for parallelisation in Shared Memory architectures by using data analysis and loop source-to-source transformations. Our optimisation strategy, although designed for OpenMP directives, is sufficiently general to be used for pure Fortran code. Our algorithm has been implemented as a tool called Automatic Guidance Module (AGM), and have received high evaluation scores from our industrial partners
Michael Leuschel, Laksono Adhianto, Michael Butler, Carla Ferreira, Leonid Mikhailov
Animation and Model Checking of CSP and B using Prolog Technology
[Bibtex]In Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic, 2001.
We describe practical experiences of using a logic programming based approach to model and reason about critical systems. We argue that logic programming with co-routining, constraints, and tabling is a good foundation for developing, animating, and model checking new specification languages. We present animators and model checkers currently being developed for two different extensions of CSP and for the B method.
Performance-Oriented Refinement
[Bibtex]PhD Thesis, Electronics and Computer Science, University of Southampton, 2001.
We introduce the probabilistic action system formalism which combines refinement with performance. Performance is expressed by means of probability and expected costs. Probability is needed to express uncertainty present in physical environments. Expected costs express physical or abstract quantities that describe a system. They encode the performance objective. The behaviour of probabilistic action systems is described by traces of expected costs. Corresponding notions of refinement and simulation-based proof rules are introduced. Formal notations like B or action systems support a notion of refinement. Refinement relates an abstract specification AA to a more deterministic concrete specification CC. Knowing AA and CC one proves CC refines, or implements, specification AA. In this study we consider specification AA as given and concern ourselves with a way to find a good candidate for implementation CC. To this end we classify all implementations of an abstract specification according to their performance. The performance of a specification AA is a value val.AA associated with some optimal behaviour it may exhibit. We distinguish performance from correctness. Concrete systems that do not meet the abstract specification are excluded. Only the remaining correct implementations CC are considered with respect to their performance. A good implementation of a specification is identified by having some optimal behaviour in common with it. In other words, a good refinement corresponds to a reduction of non-optimal behaviour. This also means that the abstract specification sets a boundary val.AA for the performance of any implementation. An implementation may perform worse than its specification but never better. Probabilistic action systems are based on discrete-time Markov decision processes. Numerical methods solving the optimisation problems posed by Markov decision processes are well-known, and used in a software tool that we have developed. The tool computes an optimal behaviour of a specification AA, and the associated value val.AA, thus assisting in the search for a good implementation CC. We present examples and case studies to demonstrate the use of probabilistic action systems.
Michael Leuschel, Andreas Podelski, C.R. Ramakrishnan, Ulrich Ultes-Nitsche (eds.)
Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic VCL'2001
[Bibtex]2001.
2000
Coverability of Reset Petri Nets and other Well-Structured Transition Systems by Partial Deduction
[PDF] [Bibtex]In Computational Logic, volume 1861 of Lecture Notes in Computer Science, 2000.
In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. It has also been shown that partial deduction is powerful enough to mimic certain algorithms to decide coverability properties of Petri nets. These algorithms are forward algorithms and hard to scale up to deal with more complicated systems. Recently, it has been proposed to use a backward algorithm scheme instead. This scheme is applicable to so-called well-structured transition systems and was successfully used, e.g., to solve coverability problems for reset Petri nets. In this paper, we discuss how partial deduction can mimic many of these backward algorithms as well. We prove this link in particular for reset Petri nets and Petri nets with transfer and doubling arcs. We thus establish a surprising link between algorithms in Petri net theory and program specialisation, and also shed light on the power of using logic program specialisation for infinite state model checking.
Decidability Results for the Propositional Fluent Calculus
[Bibtex]In Computational Logic, volume 1861 of Lecture Notes in Computer Science, Springer-Verlag, 2000.
In LPAR, volume 1955 of Lecture Notes in Computer Science, Springer-Verlag, 2000.
Solving Coverability Problems of Petri Nets by Partial Deduction
[PDF] [Bibtex]In PPDP, ACM Press, 2000.
In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. This paper focuses on one particular class of problem-coverability for (infinite state) Petri nets-and shows how existing techniques and tools for declarative programs can be successfully applied. In particular, we show that a restricted form of partial deduction is already powerful enough to decide all coverability properties of Petri Nets. We also prove that two particular instances of partial deduction exactly compute the Karp-Miller tree as well as Finkel's minimal coverability set. We thus establish an interesting link between algorithms for Petri nets and logic program specialisation.
LTL Model Checking of CSP by Refinement: How to Make FDR Spin
[Bibtex]In Proceedings VCL'2000, 2000.
We show how to (and how not to) perform LTL model checking of CSP processes using refinement checking in general and the FDR tool in particular. We show how one can handle (potentially) deadlocking systems, discuss the validity of our approach for infinite state systems, and shed light on the relationship between ``classical'' model checking and refinement checking.
Michael Leuschel, Andreas Podelski, C.R. Ramakrishnan, Ulrich Ultes-Nitsche (eds.)
Proceedings of the Workshop on Verification and Computational Logic VCL'2000
[Bibtex]2000.
The aim of this workshop is to bring together researchers working on the interplay between verification techniques (e.g., model checking, reduction, and abstraction) and logic programming techniques (e.g., constraints, abstract interpretation, program transformation).
Control Issues in Partial Deduction: The Ever Ending Story
[Bibtex]Technical Report, University of Southampton, 2000.
Partial deduction is a source-to-source technique for specialising logic programs. This is (mostly) done by a well-automated application of parts of the Burstall and Darlington unfold/fold transformation framework. One of the main challenges of partial deduction is automatic control, which has to ensure correctness, efficiency, and termination. In this survey and tutorial, we present the essential developments over the past 10 years, and discuss their respective merits and shortcomings. We also present the current state of the art and discuss areas where further research is needed to enable more widespread practical use of partial deduction and realise its potential as a tool for systematic program development.
1999
Danny De Schreye, Robert Glueck, Jesper Jørgensen,
Michael Leuschel, Bern Martens, Morten H. Sørensen
Conjunctive Partial Deduction: Foundations, Control, Algorithms, and Experiments
[PDF] [Bibtex]Journal of Logic Programming, 41(2-3): 231-277, 1999.
Efficient Specialisation in Prolog Using the Hand-Written Compiler Generator LOGEN
[Bibtex]Electronic Notes in Theoretical Computer Science, 30(2): 157-162, 1999.
Abstraction-Based Partial Deduction for Solving Inverse Problems - A Transformational Approach to Software Verification
[Bibtex]In Ershov Memorial Conference, volume 1755 of Lecture Notes in Computer Science, Springer-Verlag, 1999.
In Ershov Memorial Conference, volume 1755 of Lecture Notes in Computer Science, Springer-Verlag, 1999.
Infinite State Model Checking by Abstract Interpretation and Program Specialisation
[PDF] [Bibtex]In LOPSTR '99, volume 1817 of Lecture Notes in Computer Science, Springer-Verlag, 1999.
We illustrate the use of logic programming techniques for finite model checking of CTL formulae. We present a technique for infinite state model checking of safety properties based upon logic program specialisation and analysis techniques. The power of the approach is illustrated on several examples. For that, the efficient tools logen and ecce are used. We discuss how this approach has to be extended to handle more complicated infinite state systems and to handle arbitrary CTL formulae.
In Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School, Springer-Verlag, 1999.
In Partial Evaluation: Practice and Theory, volume 1706 of Lecture Notes in Computer Science, Springer-Verlag, 1999.
P. Hartel, Michael Butler, Andrew Currie, P. Henderson,
Michael Leuschel, A. Martin, A. Smith, Ulrich Ultes-Nitsche, R.J. Walters
Questions and Answers About Ten Formal Methods
[Bibtex]In Proc. 4th Int. Workshop on Formal Methods for Industrial Critical Systems, STAR/CNR, Pisa, Italy, 1999.
An abstract model of an industrial distributed data base application has been studied using process based, state based, and queueing theory based methods. The methods supported by graphical notations and/or integrated development environments were found to be easiest to work with. The methods supported by model checkers were the most successful in obtaining relevant information about the application. Applying a number of different methods to study one particular model encourages a problem to be viewed from different angles. This gives complementary information about the model. We report on a variety of problems of the model found through various routes. Our main conclusion is that asking experts to apply different methods and tools at a sufficiently abstract level can be done effectively revealing a broad range of information about the considered application.
Analyzing Context-Free and Context-Sensitive Grammars by Abstract Interpretation
[Bibtex]In Proceedings of the Formal Grammar Conference FG'99, University of Utrecht, 1999.
Int. Workshop on Optimization and Implementation of Declarative Programs
[Bibtex]1999.
Efficient Specialisation in Prolog Using a Hand-Written Compiler Generator
[Bibtex]Technical Report, No. DSSE-TR-99-6, University of Southampton, 1999.
Technical Report, Electronics and Computer Science, University of Southampton, 1999.
Existing refinement frameworks such as B allow a developer to specify a system on an abstract level. Subsequently, this abstract specification is refined into an implementation that performs the specified task. In this paper a conventional refinement approach is extended with a means for performance analysis. This new approach guides a developer towards well-performing implementations throughout the refinement process. The main achievement of this work is an elaboration of a connection between performance and trace refinement.
1998
Constrained Partial Deduction and the Preservation of Characteristic Trees
[Bibtex]New Generation Computing, 16(3): 283-342, 1998.
Controlling Generalisation and Polyvariance in Partial Deduction of Normal Logic Programs
[Bibtex]ACM Transactions on Programming Languages and Systems, 20(1): 208-258, 1998.
Creating Specialised Integrity Checks Through Partial Evaluation of Meta-interpreters
[PDF] [Bibtex]Journal of Logic Programming, 36(2): 149-193, 1998.
Extending Partial Deduction to Tabled Execution: Some Results and Open Issues
[Bibtex]ACM Computing Surveys, 30(3es), 1998.
Some Achievements and Prospects in Partial Deduction
[Bibtex]ACM Computing Surveys, 30(3es), 1998.
A Polyvariant Binding-Time Analysis for Off-line Partial Deduction
[PDF] [Bibtex]In ESOP, volume 1381 of Lecture Notes in Computer Science, Springer-Verlag, 1998.
Program Specialisation and Abstract Interpretation Reconciled
[PDF] [Bibtex]In IJCSLP, MIT Press, 1998.
Preserving Termination of Tabled Logic Programs While Unfolding
[PDF] [Bibtex]In LOPSTR '97, volume 1463 of Lecture Notes in Computer Science, Springer-Verlag, 1998.
Stefaan Decorte, Danny De Schreye,
Michael Leuschel, Bern Martens, Konstantinos Sagonas
In LOPSTR '97, volume 1463 of Lecture Notes in Computer Science, Springer-Verlag, 1998.
Improving Homeomorphic Embedding for Online Termination
[PDF] [Bibtex]In LOPSTR '98, volume 1559 of Lecture Notes in Computer Science, Springer-Verlag, 1998.
On the Power of Homeomorphic Embedding for Online Termination
[PDF] [Bibtex]In Proceedings SAS, volume 1503 of Lecture Notes in Computer Science, Springer-Verlag, 1998.
1997
Advanced Techniques for Logic Program Specialisation
[Bibtex]AI Communications, 10(2): 127-128, 1997.
Specialization of Declarative Programs and its Application (workshop overview)
[Bibtex]In ILPS, MIT Press, 1997.
The Ecce Partial Deduction System
[Bibtex]In Proceedings of the ILPS'97 Workshop on Tools and Environments for (Constraint) Logic Programming, 1997.
Carl von Ossietzky Universität Oldenburg, 1997.
CSP-Z ist eine Sprache zur Spezifikation zustandsbasierter kommunizierender Systeme, welche die Prozeßalgebra CSP und die Z-Notation zusammenführt. Die Semantik von CSP-Z-Spezifikationen wird durch das Failures/Divergences-Modell von CSP beschrieben, das von Roscoe angepaßt wurde, um unbeschränkten Nichtdetermismus besser behandeln zu können. Für CSP gibt es eine Verfeinerungstheorie, die auf dem Failures/Divergences-Modell basiert. Diese Theorie lässt sich in einfacher Weise auf CSP-Z übertragen. Ziel dieser Arbeit ist es die existierende Verfeinerungstheorie von Z für CSP-Z nutzbar zu machen. Mit Z können Datentypen prädikativ beschrieben werden, die nicht oder nur mit großem Aufwand zu implementieren sind. Doch bieten diese Datentypen den Vorteil, daß sie zu leichter verständlichen Spezifikationen führen, da bei starker Abstraktion viele für die Funktionalität des zu entwickelnden Programms unwesentliche Details wegfallen. Zu einem späteren Zeitpunkt werden jedoch besser implementierbare Datentypen benötigt. Es ist in Z möglich, einen (abstrakten) Datentypen durch einen anderen (konkreten) Datentypen zu ersetzen, so daß Programme, die bei Verwendung des abstrakten Datentypen korrekt waren, es auch bei Verwendung des konkreten Datentypen bleiben. Dieses Verfahren heißt Datenverfeinerung. Als Beweismethode zum Nachweis einer Datenverfeinerung dient die Simulation. Bis zu einem gewissen Grade lässt sich die Datenverfeinerungstheorie auch im Zusammenhang mit unsichtbaren Operationen verwenden, die durch Hiding entstehen. Es werden einige Regeln entwickelt, die auf den Regeln zur Datenverfeinerung in Z basieren und benutzt werden können, um Simulationsbeziehungen zwischen CSP-Z-Spezifikationen zu beweisen. Die Anwendung der entwickelten Regeln wird anhand kleinerer Fallstudien veranschaulicht.
Advanced Techniques for Logic Program Specialisation
[PDF] [Bibtex]PhD Thesis, K.U. Leuven, 1997.
Proceedings of the ILPS'97 Workshop on Specialisation of Declarative Programs and its Application
[Bibtex]1997.
1996
Efficiently Generating Efficient Generating Extensions in Prolog
[PDF] [Bibtex]In Dagstuhl Seminar on Partial Evaluation, volume 1110 of Lecture Notes in Computer Science, Springer-Verlag, 1996.
Global Control for Partial Deduction through Characteristic Atoms and Global Trees
[PDF] [Bibtex]In Dagstuhl Seminar on Partial Evaluation, volume 1110 of Lecture Notes in Computer Science, Springer-Verlag, 1996.
A Conceptual Embedding of Folding into Partial Deduction: Towards a Maximal Integration
[PDF] [Bibtex]In JICSLP, MIT Press, 1996.
In LOPSTR, volume 1207 of Lecture Notes in Computer Science, Springer-Verlag, 1996.
Logic Program Specialisation: How To Be More Specific (abstract)
[Bibtex]In LOPSTR, volume 1207 of Lecture Notes in Computer Science, Springer-Verlag, 1996.
Redundant Argument Filtering of Logic Programs
[Bibtex]In LOPSTR, volume 1207 of Lecture Notes in Computer Science, Springer-Verlag, 1996.
Specialised Integrity Checking by Combining Conjunctive Partial Deduction and Abstract Interpretation
[Bibtex]In Proc. Logic Databases and the Meaning of Change: Dagstuhl-Seminar-Report 157, IBFI GmbH, Schloss Dagstuhl, 1996.
Logic Program Specialisation: How To Be More Specific
[PDF] [Bibtex]In Proceedings PLILP'96, volume 1140 of Lecture Notes in Computer Science, Springer-Verlag, 1996.
Inspection and Feature Extraction of Marine Propellers
[Bibtex] Massachusetts Institute of Technology, 1996.
Localization Localization is the process of determining the rigid-body translations and rotations that must be performed on a set of points measured on a manufactured surface (like a propeller blade) to move those points into the closest correspondence with the ideal design surface. An additional parameter is an offset distance, such that the Euclidean motion brings the measured points as close as possible to an offset of the design surface. An algorithm to determine the seven parameters (three rotations, three translations, one offset) was developed in 1991 by R. A. Jinkerson. But that algorithm makes some assumptions about the surface and the measured points, which are sometimes not fulfilled. Specifically, it assumes, that a measured point has always an orthogonal projection on the offset surface, regardless of the translation and rotation parameters. This thesis extends Jinkerson's algorithm, so that these assumptions are not necessary any longer. This involves the development of a new objective function and its gradient.
Feature extraction During the manufacturing process, a propeller blade surface is subject to manufacturing inaccuracies, that result in small changes to the data describing its features. It is therefore desirable to recompute these features for comparison with the original design data. Most of the characteristics of a propeller blade are embedded in the camber lines of its hydrofoil sections. The objective of this part of the thesis is to recompute the camber line from a hydrofoil shape curve. An algorithm for this task has already been developed, but it makes the assumption that the blade thickness has a single maximum, which is often not fulfilled, especially, if the hydrofoil has been generated from measured data. In this thesis, a new algorithm has been developed. It generates a highly accurate camber line by using a two pass iteration method: The first pass generates an approximation of the camber line, and the second pass refines this approximation to the desired accuracy.
1995
Partial Deduction of the Ground Representation and its Application to Integrity Checking
[Bibtex]In ILPS, MIT Press, 1995.
Tutorial on Program Specialisation (abstract)
[Bibtex]In ILPS, MIT Press, 1995.
Towards Creating Specialised Integrity Checks Through Partial Evaluation of Meta-Interpreters
[PDF] [Bibtex]In PEPM, ACM Press, 1995.
Obtaining Specialised Update Procedures through Partial Deduction of the Ground Representation
[Bibtex]In Proc. Joint Workshop on Deductive Databases and Logic Programming and Abduction in Deductive Databases and Knowledge Based Systems, GMD-Studien Nr. 266, 1995.
1994
Partial Evaluation of the "Real Thing"
[Bibtex]In LOPSTR, volume 883 of Lecture Notes in Computer Science, Springer-Verlag, 1994.
