Skip to main content
main-content

Über dieses Buch

This book constitutes the refereed proceedings of the 13th International Colloquium on Theoretical Aspects of Computing, ICTAC 2016, held in Taipei, Taiwan, in October 2016.

The 23 revised full papers presented together with two short papers, two invited papers and one abstract of an invited paper were carefully reviewed and selected from 60 submissions. The papers are organized in topical sections on program verification; design, synthesis and testing; calculi; specifications; composition and transformation; automata; temporal logics; tool and short papers.

Inhaltsverzeichnis

Frontmatter

Invited Papers

Frontmatter

Verification of Concurrent Programs on Weak Memory Models

Modern multi-core processors equipped with weak memory models seemingly reorder instructions (with respect to program order) due to built-in optimizations. For concurrent programs, weak memory models thereby produce interleaved executions which are impossible on sequentially consistent (SC) memory. Verification of concurrent programs consequently needs to take the memory model of the executing processor into account. This, however, makes most standard software verification tools inapplicable.
In this paper, we propose a technique (and present its accompanying tool Weak2SC) for reducing the verification problem for weak memory models to the verification on SC. The reduction proceeds by generating – out of a given program and weak memory model (here, TSO or PSO) – a new program containing all reorderings, thus already exhibiting the additional interleavings on SC. Our technique is compositional in the sense that program generation can be carried out on single processes without ever needing to inspect the state space of the concurrent program. We formally prove compositionality as well as soundness of our technique.
Weak2SC takes standard C programs as input and produces program descriptions which can be fed into automatic model checking tools (like SPIN) as well as into interactive provers (like KIV). Thereby, we allow for a wide range of verification options. We demonstrate the effectiveness of our technique by evaluating Weak2SC on a number of example programs, ranging from concurrent data structures to software transactional memory algorithms.
Oleg Travkin, Heike Wehrheim

Petri Nets and Semilinear Sets (Extended Abstract)

Semilinear sets play a key role in many areas of computer science, in particular, in theoretical computer science, as they are characterizable by Presburger Arithmetic (a decidable theory). The reachability set of a Petri net is not semilinear in general. There are, however, a wide variety of subclasses of Petri nets enjoying semilinear reachability sets, and such results as well as analytical techniques developed around them contribute to important milestones historically in the analysis of Petri nets. In this talk, we first give a brief survey on results related to Petri nets with semilinear reachability sets. We then focus on a technique capable of unifying many existing semilinear Petri nets in a coherent way. The unified strategy also leads to various new semilinearity results for Petri nets. Finally, we shall also briefly touch upon the notion of almost semilinear sets which witnesses some recent advances towards the general Petri net reachability problem.
Hsu-Chun Yen

Program Verification

Frontmatter

Termination of Single-Path Polynomial Loop Programs

Termination analysis of polynomial programs plays a very important role in applications of safety critical software. In this paper, we investigate the termination problem of single-path polynomial loop programs (SPLPs) over the reals. For such a loop program, we first assume that the set characterized by its loop guards is closed, bounded and connected. And then, we give some conditions and prove that under such conditions, the termination of single-path loop programs is decidable over the reals.
Yi Li

Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm

We formally prove the correctness of Prim’s algorithm for computing minimum spanning trees. We introduce new generalisations of relation algebras and Kleene algebras, in which most of the proof can be carried out. Only a small part needs additional operations, for which we introduce a new algebraic structure. We instantiate these algebras by matrices over extended reals, which model the weighted graphs used in the algorithm. Many existing results from relation algebras and Kleene algebras generalise from the relation model to the weighted-graph model with no or small changes. The overall structure of the proof uses Hoare logic. All results are formally verified in Isabelle/HOL heavily using its integrated automated theorem provers.
Walter Guttmann

Certified Impossibility Results and Analyses in Coq of Some Randomised Distributed Algorithms

Randomised algorithms are generally simple to formulate. However, their analysis can become very complex, especially in the field of distributed computing. In this paper, we formally model in Coq a class of randomised distributed algorithms. We develop some tools to help proving impossibility results about classical problems and analysing this class of algorithms. As case studies, we examine the handshake and maximal matching problems. We show how to use our tools to formally prove properties about algorithms solving those problems.
Allyx Fontaine, Akka Zemmari

Calculating Statically Maximum Log Memory Used by Multi-threaded Transactional Programs

During the execution of multi-threaded and transactional programs, when new threads are created or new transactions are started, memory areas called logs are implicitly allocated to store copies of shared variables so that the threads can independently manipulate these variables. It is not easy to manually calculate the peak of memory allocated for logs when programs have arbitrary mixes of nested transactions and new thread creations. We develop a static analysis to compute the amount of memory used by logs in the worst execution scenarios of the programs. We prove the soundness of our analysis and we show a prototype tool to infer the memory bound.
Anh-Hoang Truong, Ngoc-Khai Nguyen, Dang Van Hung, Duc-Hanh Dang

Design, Synthesis and Testing

Frontmatter

Synthesis of Petri Nets with Whole-Place Operations and Localities

Synthesising systems from behavioural specifications is an attractive way of constructing implementations which are correct-by-design and thus requiring no costly validation efforts. In this paper, systems are modelled by Petri nets and the behavioural specifications are provided in the form of step transition systems, where arcs are labelled by multisets of executed actions. We focus on the problem of synthesising Petri nets with whole-place operations and localities (wpol-nets), which are a class of Petri nets powerful enough to express a wide range of system behaviours, including inhibition of actions, resetting of local states, and locally maximal executions.
The synthesis problem was solved for several specific net classes and later a general approach was developed within the framework of \(\tau \)-nets. In this paper, we follow the synthesis techniques introduced for \(\tau \)-nets that are based on the notion of a region of a transition system, which we suitably adapt to work for wpol-nets.
Jetty Kleijn, Maciej Koutny, Marta Pietkiewicz-Koutny

Schedulers and Finishers: On Generating the Behaviours of an Event Structure

It is well known that every trace of a transition system can be generated using a scheduler. However, this basic completeness result does not hold in event structure models. The reason for this failure is that, according to its standard definition, a scheduler chooses which action to schedule and, at the same time, finishes the one scheduled last. Thus, scheduled events will never be able to overlap. We propose to separate scheduling from finishing and introduce the dual notion of finishers which, together with schedulers, are enough to regain completeness back. We then investigate all possible interactions between schedulers and finishers, concluding that simple alternating interactions are enough to express complex ones. Finally, we show how finishers can be used to filter behaviours to the extent to which they capture intrinsic system characteristics.
Annabelle McIver, Tahiry Rabehaja, Georg Struth

On the Expressiveness of Symmetric Communication

The expressiveness of communication primitives has been explored in a common framework based on the \(\pi \)-calculus by considering four features: synchronism, arity, communication medium, and pattern-matching. These all assume asymmetric communication between input and output primitives, however some calculi consider more symmetric approaches to communication such as fusion calculus and Concurrent Pattern Calculus. Symmetry can be considered either as supporting exchange of information between an action and co-action, or as unification of actions. By means of possibility/impossibility of encodings, this paper shows that the exchange approach is related to, or more expressive than, many previously considered languages. Meanwhile, the unification approach is more expressive than some, but mostly unrelated to, other languages.
Thomas Given-Wilson, Axel Legay

Towards MC/DC Coverage of Properties Specification Patterns

Model based testing is used to validate the actual system against its requirements described as formal specification, while formal verification proves that a requirement is not violated in the overall system. Verifying properties, in certain cases, becomes very expensive (or unpractical), mainly when the application of test techniques is enough for the users purposes. The Modified Condition/Decision Coverage (MC/DC), used in the avionics software industry, is recognised as a good technique to find out the possible mistakes on programs logics because it covers how each condition can affect the programs’ decisions outcomes. It has also been adapted to provide the coverage of specifications in the requirements-based approach.
This paper proposes a technique to decompose properties (specifications), defined as regular expressions, into subexpressions representing test cases to cover the MD/DC for specifications (Unique First Word Recognition). Then, instead of proving an entire property, we can use a model checker to observe and select program executions that cover all the test cases given as the subexpressions. To support this approach, we give a syntactic characterisation of the properties decomposition, inductively defined over the syntax of regular expressions, and show how to use the technique to decompose Specification Patterns (SPS) and monitor their satisfiability using the Java PathFinder (JPF).
Ana C. V. de Melo, Corina S. Păsăreanu, Simone Hanazumi

Calculi

Frontmatter

Unification for -calculi Without Propagation Rules

We present a unification procedure for calculi with explicit substitutions (ES) without propagation rules. The novelty of this work is that the unification procedure was developed for the calculi with ES that belong to the paradigm known as “act at a distance”, i.e. explicit substitutions are not propagated to the level of variables, as usual. The unification procedure is proved correct and complete, and enjoy a simple form of substitution, called grafting, instead of the standard capture avoiding variable substitution.
Flávio L. C. de Moura

Soundly Proving B Method Formulæ Using Typed Sequent Calculus

The B Method is a formal method mainly used in the railway industry to specify and develop safety-critical software. To guarantee the consistency of a B project, one decisive challenge is to show correct a large amount of proof obligations, which are mathematical formulæ expressed in a classical set theory extended with a specific type system. To improve automated theorem proving in the B Method, we propose to use a first-order sequent calculus extended with a polymorphic type system, which is in particular the output proof-format of the tableau-based automated theorem prover Zenon. After stating some modifications of the B syntax and defining a sound elimination of comprehension sets, we propose a translation of B formulæ into a polymorphic first-order logic format. Then, we introduce the typed sequent calculus used by Zenon, and show that Zenon proofs can be translated to proofs of the initial B formulæ in the B proof system.
Pierre Halmagrand

Deriving Inverse Operators for Modal Logic

Spatial constraint systems are algebraic structures from concurrent constraint programming to specify spatial and epistemic behavior in multi-agent systems. We shall use spatial constraint systems to give an abstract characterization of the notion of normality in modal logic and to derive right inverse/reverse operators for modal languages. In particular, we shall identify the weakest condition for the existence of right inverses and show that the abstract notion of normality corresponds to the preservation of finite suprema. We shall apply our results to existing modal languages such as the weakest normal modal logic, Hennessy-Milner logic, and linear-time temporal logic. We shall discuss our results in the context of modal concepts such as bisimilarity and inconsistency invariance.
Michell Guzmán, Salim Perchy, Camilo Rueda, Frank D. Valencia

Specifications

Frontmatter

Specifying Properties of Dynamic Architectures Using Configuration Traces

The architecture of a system describes the system’s overall organization into components and connections between those components. With the emergence of mobile computing, dynamic architectures became increasingly important. In such architectures, components may appear or disappear, and connections may change over time.
Despite the growing importance of dynamic architectures, the specification of properties for those architectures remains a challenge. To address this problem, we introduce the notion of configuration traces to model properties of dynamic architectures. Then, we investigate these properties to identify different types thereof. We show completeness and consistency of these types, i.e., we show that (almost) every property can be separated into these types and that a property of one type does not impact properties of other types.
Configuration traces can be used to specify general properties of dynamic architectures and the separation into different types provides a systematic way for their specification. To evaluate our approach we apply it to the specification and verification of the Blackboard pattern in Isabelle/HOL.
Diego Marmsoler, Mario Gleirscher

Behavioural Models for FMI Co-simulations

Simulation is a favoured technique for analysis of cyber-physical systems. With their increase in complexity, co-simulation, which involves the coordinated use of heterogeneous models and tools, has become widespread. An industry standard, FMI, has been developed to support orchestration; we provide the first behavioural semantics of FMI. We use the state-rich process algebra, \({{\textsf {\textit{Circus}}}}\), to present our modelling approach, and indicate how models can be automatically generated from a description of the individual simulations and their dependencies. We illustrate the work using three algorithms for orchestration. A stateless version of the models can be verified using model checking via translation to CSP. With that, we can prove important properties of these algorithms, like termination and determinism, for example. We also show that the example provided in the FMI standard is not a valid algorithm.
Ana Cavalcanti, Jim Woodcock, Nuno Amálio

An Abstract Model for Proving Safety of Autonomous Urban Traffic

The specification of Multi-lane Spatial Logic (MLSL) was introduced in [1, 2] for proving safety (collision freedom) on multi-lane motorways and country roads. We now consider an extension of MLSL to deal with urban traffic scenarios, thereby focusing on crossing manoeuvres at intersections. To this end, we modify the existing abstract model by introducing a generic topology of urban traffic networks. We then show that even at intersections we can use purely spatial reasoning, detached from the underlying car dynamics, to prove safety of controllers modelled as extended timed automata.
Martin Hilscher, Maike Schwammberger

Composition and Transformation

Frontmatter

Unifying Heterogeneous State-Spaces with Lenses

Most verification approaches embed a model of program state into their semantic treatment. Though a variety of heterogeneous state-space models exists, they all possess common theoretical properties one would like to capture abstractly, such as the common algebraic laws of programming. In this paper, we propose lenses as a universal state-space modelling solution. Lenses provide an abstract interface for manipulating data types through spatially-separated views. We define a lens algebra that enables their composition and comparison, and apply it to formally model variables and alphabets in Hoare and He’s Unifying Theories of Programming (UTP). The combination of lenses and relational algebra gives rise to a model for UTP in which its fundamental laws can be verified. Moreover, we illustrate how lenses can be used to model more complex state notions such as memory stores and parallel states. We provide a mechanisation in Isabelle/HOL that validates our theory, and facilitates its use in program verification.
Simon Foster, Frank Zeyda, Jim Woodcock

Ensuring Correctness of Model Transformations While Remaining Decidable

This paper is concerned with the interplay of the expressiveness of model and graph transformation languages, of assertion formalisms making correctness statements about transformations, and the decidability of the resulting verification problems. We put a particular focus on transformations arising in graph-based knowledge bases and model-driven engineering. We then identify requirements that should be satisfied by logics dedicated to reasoning about model transformations, and investigate two promising instances which are decidable fragments of first-order logic.
Jon Haël Brenas, Rachid Echahed, Martin Strecker

ProofScript: Proof Scripting for the Masses

The goal of the ProofPeer project is to make collaborative theorem proving a reality. An important part of our plan to make this happen is ProofScript, a language designed to be the main user interface of ProofPeer. Of foremost importance in the design of ProofScript is its fit within a collaborative theorem proving environment. By this we mean that it needs to fit into an environment where peers who are not necessarily part of the current theorem proving and programming language communities work independently from but collaboratively with each other to produce formal definitions and proofs. All aspects of ProofScript are shaped by this design principle. In this paper we will discuss ProofScript’s most important aspect of being an integrated language both for interactive proof and for proof scripting.
Steven Obua, Phil Scott, Jacques Fleuriot

Automata

Frontmatter

Derived-Term Automata for Extended Weighted Rational Expressions

We present an algorithm to build an automaton from a rational expression. This approach introduces support for extended weighted expressions. Inspired by derived-term based algorithms, its core relies on a different construct, rational expansions. We introduce an inductive algorithm to compute the expansion of an expression from which the automaton follows. This algorithm is independent of the size of the alphabet, and actually even supports infinite alphabets. It can easily be accommodated to generate deterministic (weighted) automata. These constructs are implemented in Vcsn, a free-software platform dedicated to weighted automata and rational expressions.
Akim Demaille

Weighted Register Automata and Weighted Logic on Data Words

In this paper, we investigate automata models for quantitative aspects of systems with infinite data domains, e.g., the costs of storing data on a remote server or the consumption of resources (e.g., memory, energy, time) during a data analysis. We introduce weighted register automata on data words and investigate their closure properties. In our main result, we give a logical characterization of weighted register automata by means of weighted existential monadic second-order logic; for the proof we employ a new class of determinizable visibly register automata.
Parvaneh Babari, Manfred Droste, Vitaly Perevoshchikov

Hybrid Automata as Coalgebras

Able to simultaneously encode discrete transitions and continuous behaviour, hybrid automata are the de facto framework for the formal specification and analysis of hybrid systems. The current paper revisits hybrid automata from a coalgebraic point of view. This allows to interpret them as state-based components, and provides a uniform theory to address variability in their definition, as well as the corresponding notions of behaviour, bisimulation, and observational semantics.
Renato Neves, Luis S. Barbosa

Temporal Logics

Frontmatter

Temporal Logic Verification for Delay Differential Equations

Delay differential equations (DDEs) play an important role in the modeling of dynamic processes. Delays may arise in contemporary control schemes like networked distributed control and may cause deterioration of control performance, invalidating both stability and safety properties. This induces an interest in DDE especially in the area of modeling embedded control and formal methods for its verification. In this paper, we present an approach aiming at automatic safety verification of a simple class of DDEs against requirements expressed in a linear-time temporal logic. As requirements specification language, we exploit metric interval temporal logic (MITL) with a continuous-time semantics evaluating signals over metric spaces. We employ an interval-based Taylor over-approximation method to enclose the solution of the DDE. As the solution of the DDE gets represented as a timed state sequence in terms of the Taylor coefficients, we can effectively solve temporal-logic verification problems represented as time-bounded MITL formulae. We encode necessary conditions for their satisfaction as SMT formulae over polynomial arithmetic and use the iSAT3 SMT solver in its bounded model checking mode for discharging the resulting proof obligations, thus proving satisfaction of MITL specifications by the trajectories induced by a DDE. In contrast to our preliminary work in [34], we can verify arbitrary time-bounded MITL formulae, including nesting of modalities, rather than just invariance properties.
Peter Nazier Mosaad, Martin Fränzle, Bai Xue

Dynamic Logic with Binders and Its Application to the Development of Reactive Systems

This paper introduces a logic to support the specification and development of reactive systems on various levels of abstraction, from property specifications, concerning e.g. safety and liveness requirements, to constructive specifications representing concrete processes. This is achieved by combining binders of hybrid logic with regular modalities of dynamic logics in the same formalism, which we call \(\mathcal {D}^{\downarrow }\)-logic. The semantics of our logic focuses on effective processes and is therefore given in terms of reachable transition systems with initial states. The second part of the paper resorts to this logic to frame stepwise development of reactive systems within the software development methodology proposed by Sannella and Tarlecki. In particular, we instantiate the generic concepts of constructor and abstractor implementations by using standard operators on reactive components, like relabelling and parallel composition, as constructors, and bisimulation for abstraction. We also study vertical composition of implementations which relies on the preservation of bisimularity by the constructions on labeleld transition systems.
Alexandre Madeira, Luis S. Barbosa, Rolf Hennicker, Manuel A. Martins

Propositional Dynamic Logic for Petri Nets with Iteration

This work extends our previous work [20] with the iteration operator. This new operator allows for representing more general networks and thus enhancing the former propositional logic for Petri Nets. We provide an axiomatization and a new semantics and prove soundness and completeness with respect with its semantics. In order to illustrate its usage, we also provide some examples.
Mario R. F. Benevides, Bruno Lopes, Edward Hermann Haeusler

Tool and Short Papers

Frontmatter

ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti

The programming environment FoCaLiZe allows the user to specify, implement, and prove programs with the help of the theorem prover Zenon. In the actual version, those proofs are verified by Coq. In this paper we propose to extend the FoCaLiZe compiler by a backend to the Dedukti language in order to benefit from Zenon Modulo, an extension of Zenon for Deduction modulo. By doing so, FoCaLiZe can benefit from a technique for finding and verifying proofs more quickly. The paper focuses mainly on the process that overcomes the lack of local pattern-matching and recursive definitions in Dedukti.
Raphaël Cauderlier, Catherine Dubois

Parametric Deadlock-Freeness Checking Timed Automata

Distributed real-time systems are notoriously difficult to design, and must be verified, e. g., using model checking. In particular, deadlocks must be avoided as they either yield a system subject to potential blocking, or denote an ill-formed model. Timed automata are a powerful formalism to model and verify distributed systems with timing constraints. In this work, we investigate synthesis of timing constants in timed automata for which the model is guaranteed to be deadlock-free.
Étienne André

Backmatter

Weitere Informationen

Premium Partner

BranchenIndex Online

Die B2B-Firmensuche für Industrie und Wirtschaft: Kostenfrei in Firmenprofilen nach Lieferanten, Herstellern, Dienstleistern und Händlern recherchieren.

Whitepaper

- ANZEIGE -

Best Practices für die Mitarbeiter-Partizipation in der Produktentwicklung

Unternehmen haben das Innovationspotenzial der eigenen Mitarbeiter auch außerhalb der F&E-Abteilung erkannt. Viele Initiativen zur Partizipation scheitern in der Praxis jedoch häufig. Lesen Sie hier  - basierend auf einer qualitativ-explorativen Expertenstudie - mehr über die wesentlichen Problemfelder der mitarbeiterzentrierten Produktentwicklung und profitieren Sie von konkreten Handlungsempfehlungen aus der Praxis.
Jetzt gratis downloaden!

Bildnachweise