Search

SAT solvers decide the satisfiability of Boolean formulas in conjunctive normal form. They are commonly used for software and hardware verification. Modern SAT solvers are highly complex and optimized programs. As a single bug in the solver may invalidate the verification of many systems, SAT solvers output certificates for their answer, which are then checked independently. However, even certificate checking requires highly optimized non-trivial programs. This paper presents the first SAT solver certificate checker that is formally verified down to the integer sequence representing the formula. Our tool supports the full DRAT standard, and is even faster than the unverified state-of-the-art tool drat-trim, on a realistic set of benchmarks drawn from the 2016 and 2017 SAT competitions. An optional multi-threaded mode further reduces the runtime, in particular for big certificates. [ABSTRACT FROM AUTHOR]

Formal methods and verification tools have been in use in the engineering of safety-critical transport systems for well over 30 years. In both the railway and the avionics domain, for instance, formal methods are specifically recommended in current international certification standards for ultra-dependable systems and for products at the highest integrity level. In fact, traditionally, the applications of formal methods and tools to such transport systems concern demonstrating, with the highest levels of assurance, the correct functioning of the software systems involved, such as train signalling systems to avoid collisions. More recently, however, formal methods and verification tools have started to be applied also to the scheduling and management of transport systems or networks, for instance to optimise the exploitation of a railway line or to improve the operational efficiency of a bus network. In this introduction to the special issue on “Formal Methods for Transport Systems”, we outline some recent achievements for each of the above-mentioned types of application of formal methods and tools. These achievements are represented by three selected papers: one was selected from the “Formal Methods and Safety Certification: Challenges in the Railways Domain” track at the seventh International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016); another one was selected from the 21st International Workshop on Formal Methods for Industrial Critical Systems and the 16th International Workshop on Automated Verification of Critical Systems (FMICS-AVoCS 2016); a final one was selected after an open call for contributions. [ABSTRACT FROM AUTHOR]

We study $$\mu $$ HML, a branching-time logic with least and greatest fixpoints, from a runtime verification perspective. The logic may be used to specify properties of programs whose behaviour may be expressed as a labelled transition system. We establish which subset of this logic can be monitored for at runtime by merely observing the runtime execution of a program. A monitor-synthesis algorithm is defined for this subset, where it is shown that the resulting synthesised monitors correctly perform the required analysis from the observed behaviour. We also prove completeness results wrt. this logical subset that show that, up to logical equivalence, no other properties apart from those identified can be monitored for and verified at runtime. [ABSTRACT FROM AUTHOR]

Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The analysis is necessarily an over-approximation as the real executions of the program are not available at analysis time. In contrast, runtime verification techniques have been extensively used for control-oriented properties, analysing the current execution path of the program in a fully automatic manner. In this article, we present a novel approach in which data-oriented and control-oriented properties may be stated in a single formalism amenable to both static and dynamic verification techniques. The specification language we present to achieve this that of ppDATEs, which enhances the control-oriented property language of DATEs, with data-oriented pre/postconditions. For runtime verification of ppDATE specifications, the language is translated into a DATE. We give a formal semantics to ppDATEs, which we use to prove the correctness of our translation from ppDATEs to DATEs. We show how ppDATE specifications can be analysed using a combination of the deductive theorem prover KeY and the runtime verification tool LARVA. Verification is performed in two steps: KeY first partially proves the data-oriented part of the specification, simplifying the specification which is then passed on to LARVA to check at runtime for the remaining parts of the specification including the control-oriented aspects. We show the applicability of our approach on two case studies. [ABSTRACT FROM AUTHOR]

Programmable logic controllers are typically programmed in one of the five languages defined in the IEC 61131 standard. While the ability to choose the appropriate language for each program unit may be an advantage for the developers, it poses a serious challenge to verification methods. In this paper we analyse and compare these languages to show that the ST programming language can efficiently and conveniently represent all PLC languages for formal verification purposes. Furthermore, we provide a translation method from IL to ST programming languages (for the Siemens implementation), together with a sketch of proof for its correctness. This allows the usage of the ST-based PLCverif model checking method for safety PLC programs. [ABSTRACT FROM AUTHOR]

The behavior of practical safety critical systems often combines real-time behavior with structured data flow. To ensure correctness of such systems, both aspects have to be modeled and formally verified. Time related behavior can be efficiently modeled and analyzed in terms of timed automata. At the same time, program verification techniques like abstract interpretation and software model checking can efficiently handle data flow. In this paper, we describe a simple formalism that represents both aspects of such systems in a uniform and explicit way, thus enables the combination of formal analysis methods for real-time systems and software using standard techniques. [ABSTRACT FROM AUTHOR]

Spatial aspects of computation are becoming increasingly relevant when dealing with systems distributed in physical space. Traditional formal verification techniques are well suited to analyse the temporal evolution of system models; however, properties of space are typically not taken into account explicitly. In this position paper we briefly review some of the recent developments of spatial and spatio-temporal model-checking in the context of the European research project QUANTICOL funded by the FET-Proactive programme on Fundamentals of Collective Adaptive Systems. We illustrate some typical applications of spatial and spatio-temporal model checking on collective adaptive systems and provide an outline for further developments. [ABSTRACT FROM AUTHOR]

Computational kernels, which are small pieces of software that selectively capture the characteristics of larger applications, have been used successfully for decades. Kernels allow for the testing of a compiler's ability to optimize code, performance of future hardware and reproducing compiler bugs. Unfortunately they can be rather time consuming to create and do not always accurately represent the full complexity of large scientific applications. Furthermore, expert knowledge is often required to create such kernels. In this paper, we present a Python-based tool that greatly simplifies the generation of computational kernels from Fortran based applications. Our tool automatically extracts partial source code of a larger Fortran application into a stand-alone executable kernel. Additionally, our tool also generates state data necessary for proper execution and verification of the extracted kernel. We have utilized our tool to extract more than thirty computational kernels from a million-line climate simulation model. Our extracted kernels have been used for a variety of purposes including: code modernization, identification of limitations in compiler optimizations, numerical algorithm debugging, compiler bug reporting, and for procurement benchmarking. [ABSTRACT FROM AUTHOR]

Much of the development of model-based design and dependability analysis in the design of dependable systems, including software intensive systems, can be attributed to the application of advances in formal logic and its application to fault forecasting and verification of systems. In parallel, work on bio-inspired technologies has shown potential for the evolutionary design of engineering systems via automated exploration of potentially large design spaces. We have not yet seen the emergence of a design paradigm that effectively combines these two techniques, schematically founded on the two pillars of formal logic and biology, from the early stages of, and throughout, the design lifecycle. Such a design paradigm would apply these techniques synergistically and systematically to enable optimal refinement of new designs which can be driven effectively by dependability requirements. The paper sketches such a model-centric paradigm for the design of dependable systems, presented in the scope of the HiP-HOPS tool and technique, that brings these technologies together to realise their combined potential benefits. The paper begins by identifying current challenges in model-based safety assessment and then overviews the use of meta-heuristics at various stages of the design lifecycle covering topics that span from allocation of dependability requirements, through dependability analysis, to multi-objective optimisation of system architectures and maintenance schedules. [ABSTRACT FROM AUTHOR]

In the article [10] a formal system for Propositional Linear Temporal Logic (in short LTLB) with normal semantics is introduced. The language of this logic consists of 'until' operator in a very strict version. The very strict 'until' operator enables to express all other temporal operators. In this article we construct a formal system for LTLB with the initial semantics [12]. Initial semantics means that we define the validity of the formula in a model as satisfaction in the initial state of model while normal semantics means that we define the validity as satisfaction in all states of model. We prove the Deduction Theorem, and the soundness and completeness of the introduced formal system. We also prove some theorems to compare both formal systems, i.e., the one introduced in the article [10] and the one introduced in this article. Formal systems for temporal logics are applied in the verification of computer programs. In order to carry out the verification one has to derive an appropriate formula within a selected formal system. The formal systems introduced in [10] and in this article can be used to carry out such verifications in Mizar [4]. [ABSTRACT FROM AUTHOR]

Social commitments have been extensively and effectively used to represent and model business contracts among autonomous agents having competing objectives in a variety of areas (e.g., modeling business processes and commitment-based protocols). However, the formal verification of social commitments and their fulfillment is still an active research topic. This paper presents CTLC that modifies CTLC, a temporal logic of commitments for agent communication that extends computation tree logic (CTL) logic to allow reasoning about communicating commitments and their fulfillment. The verification technique is based on reducing the problem of model checking CTLC into the problem of model checking ARCTL (the combination of CTL with action formulae) and the problem of model checking GCTL (a generalized version of CTL with action formulae) in order to respectively use the extended NuSMV symbolic model checker and the CWB-NC automata-based model checker as a benchmark. We also prove that the reduction techniques are sound and the complexity of model checking CTLC for concurrent programs with respect to the size of the components of these programs and the length of the formula is PSPACE-complete. This matches the complexity of model checking CTL for concurrent programs as shown by Kupferman et al. We finally provide two case studies taken from business domain along with their respective implementations and experimental results to illustrate the effectiveness and efficiency of the proposed technique. The first one is about the NetBill protocol and the second one considers the Contract Net protocol. [ABSTRACT FROM AUTHOR]

This article investigates under which conditions instantiation-based proof procedures can be combined in a nested way, in order to mechanically construct new instantiation procedures for richer theories. Interesting applications in the field of verification are emphasized, particularly for handling extensions of the theory of arrays. [ABSTRACT FROM AUTHOR]

An alternative algorithm for calculation of foundation settlements is proposed for computer programs, and a procedure for, and an example of its implementation in a stepwise approximate rendering are presented. When access to computer programs is limited, application of the procedure is possible for prediction of expected settlement and verification of the results obtained. [ABSTRACT FROM AUTHOR]

For programs whose data variables range over Boolean or finite domains, program verification is decidable, and this forms the basis of recent tools for software model checking. In this article, we consider algorithmic verification of programs that use Boolean variables, and in addition, access a single read-only array whose length is potentially unbounded, and whose elements range over an unbounded data domain. We show that the reachability problem, while undecidable in general, is (1) PSPACE-complete for programs in which the array-accessing for-loops are not nested, (2) decidable for a restricted class of programs with doubly nested loops. The second result establishes connections to automata and logics defining languages over data words. [ABSTRACT FROM AUTHOR]

An Ambient Intelligence (AmI) system is a pervasive system in which services have some intelligence in order to smoothly interact with users immersed in the environment. Users are the main entity in AmI systems. Thus, the services are user-centred with an adaptive interaction that provides users with more personalized facilities in a non-intrusive way. The deployment of AmI services is a hard task, especially when the system includes complex users' behaviours or complex deployments in terms of the devices and software participating at the system. Since one of the intrinsic requirements in these services is smooth interaction with users, the user, or at least a model of the user, should be incorporated in the development process. This makes the process of verification and validation of such services quite difficult. This paper proposes the use of Agent Based Social Simulation for a quick and feasible validation of AmI systems. Simulation in the first stages enables easy validation of the services before real environment deployment. The main challenge in this approach is how to simulate humans with realistic behaviours. In this paper, Social Simulation (SS) is used to tackle this problem. Specifically, this paper presents a methodology for the validation of AmI systems by SS. The realistic modelling of users and its validation are key elements of this process and involve challenges that the techniques proposed here are able to deal with. A real application example which shows the level of reality reached in the users' models and the benefits of the methodology is presented in this paper. [ABSTRACT FROM AUTHOR]

Past studies have shown that most inertial profiler verification procedures are conducted through repeated profile measurements on test sections with known profiles. This type of an evaluation can erroneously affect inertial profile results because of non-controllable parameters such as profiler equipment, analytical software, and operator variables. In order to improve the accuracy of inertial profiler certifications, a laboratory simulation method for inertial profilers was developed. This method uses an apparatus that combines sinusoidal vertical displacements of various frequencies and amplitude levels. As a result, errors attributed to operator variables are excluded, and errors induced by a profiler and software are further identified. This study utilizes the Hilbert-Huang transform (HHT) to improve the laboratory verification process by reducing measurement noise and creating a more stable signal in different frequency-amplitude combinations. The noise source is also identified by applying the HHT, which can provide guidance on further profiler verification enhancements. [ABSTRACT FROM AUTHOR]

Software testing is particularly expensive for developers of high-assurance software, such as software that is produced for mission critical systems. One reason for this expense is the system requirement that test suites be modified to provide condition or decision coverage completely. Despite its cost, there is evidence that coverage technique is an effective verification method and can help to reduce the size of the test suite. To address the test-suite size problem, researchers have investigated the use of test-suite minimization algorithms, which identify a reduced test suite that provides the same coverage of the software according to some criterion as the original test suite, and test-suite prioritization algorithms, which identify an ordering of the test cases in the test suite according to some criteria or goals. Existing techniques for test suite minimization consider test-case coverage criteria, other criteria such as risk or fault--detection effectiveness, or combinations of these criteria, but ignore the test-execution cost because of the complexity. This paper investigates the use of swarm intelligence called Particle Swarm Optimization over conventional evolutionary approach, for this test-suite minimization problem. Unlike other algorithms, this algorithm uses new criteria, which is a combination of a block based coverage criteria and a test-execution cost criteria, to make decisions about reducing a test suite. Finally, the results generated were studied by comparing with Genetic based Test suite minimization algorithm. The outcome illustrate that this algorithm can significantly reduce the size and the cost of the test-suite for regression testing. This paper focuses on multiple objectives to reduce the test-execution cost and the size of the reduced test suite rather than only the size as done by conventional methods. [ABSTRACT FROM AUTHOR]

Verification methods for memory-manipulating C programs need to address not only well-typed programs that respect invariants such as the split-heap memory model, but also programs that access through pointers arbitrary memory objects such as local variables, single struct fields, or array slices. We present a logic for memory layouts that covers these applications and show how proof obligations arising during the verification can be discharged automatically using the layouts. The framework developed in this way is also suitable for reasoning about data structures manipulated by algorithms, which we demonstrate by verifying the Schorr-Waite graph marking algorithm. [ABSTRACT FROM AUTHOR]

Testing and Bounded Model Checking (BMC) are two techniques used in Software Verification for bug-hunting. They are expression of two different philosophies: testing is used on the compiled code and it is more suited to find errors in common behaviors, while BMC is used on the source code to find errors in uncommon behaviors of the system. Nowadays, testing is by far the most used technique for software verification in industry: it is easy to use and even when no error is found, it can release a set of tests certifying the (partial) correctness of the compiled system. In the case of safety critical software, in order to increase the confidence of the correctness of the compiled system, it is often required that the provided set of tests covers 100% of the code. This requirement, however, substantially increases the costs associated to the testing phase, since it often involves the manual generation of tests. In this paper we show how BMC can be productively applied to the Software Verification process in industry. In particular, we show how to productively use a Bounded Model Checker for C programs (CBMC) as an automatic test generator for the Coverage Analysis of Safety Critical Software. In particular, we experimented CBMC on a subset of the modules of the European Train Control System (ETCS) of the European Rail Traffic Management System (ERTMS) source code, an industrial system for the control of the traffic railway, provided by Ansaldo STS. The Code of the ERTMS/ETCS, with thousands of lines, has been used as trial application with CBMC obtaining a set of tests satisfying the target 100% code coverage, requested by the CENELEC EN50128 guidelines for software development of safety critical systems. The use of CBMC for test generation led to a dramatic increase in the productivity of the entire Software Development process by substantially reducing the costs of the testing phase. To the best of our knowledge, this is the first time that BMC techniques have been used in an industrial setting for automatically generating tests achieving full coverage of Safety-Critical Software. The positive results demonstrate the maturity of Bounded Model Checking techniques for automatic test generation in industry. [ABSTRACT FROM AUTHOR]

Abstract: An important feature of the service-oriented approach is the ability to aggregate, through programmable coordination patterns, the activities involved in service interactions. Two different approaches can be adopted to tackle service coordination: orchestration and choreography. In this paper, we introduce a formal methodology to handle coordination among services from the perspective of a global observer, in the spirit of choreography models. In particular, we address the problem of verifying compliance and consistency between the design of service interactions and the choreography constraints. [Copyright &y& Elsevier]

Perfect pre-deployment test coverage is notoriously difficult to achieve for large applications. Given enough end users, however, many more test cases will be encountered during an application's deployment than during testing. The use of runtime verification after deployment would enable developers to detect unexpected situations. Unfortunately, the prohibitive performance cost of runtime monitors prevents their use in deployed code. In this work, we study the feasibility of collaborative runtime verification, a verification approach which can distribute the burden of runtime verification among multiple users and over multiple runs. Each user executes a partially instrumented program and therefore suffers only a fraction of the instrumentation overhead. We focus on runtime verification using tracematches. Tracematches are a specification formalism that allows users to specify runtime verification properties via regular expressions with free variables over the dynamic execution trace. We propose two techniques for soundly partitioning the instrumentation required for tracematches: spatial partitioning, where different copies of a program monitor different program points for violations, and temporal partitioning, where monitoring is switched on and off over time. We evaluate the relative impact of partitioning on a user's runtime overhead by applying each partitioning technique to a collection of benchmarks that would otherwise incur significant instrumentation overhead. Our results show that spatial partitioning almost completely eliminates runtime overhead (for any particular benchmark copy) on many of our test cases, and that temporal partitioning scales well and provides runtime verification on a ‘pay as you go’ basis. [ABSTRACT FROM PUBLISHER]

Recent developments in runtime verification and monitoring show that parametric regular and temporal logic specifications can be efficiently monitored against large programs. However, these logics reduce to ordinary finite automata, limiting their expressivity. For example, neither can specify structured properties that refer to the call stack of the program. While context-free grammars (CFGs) are expressive and well-understood, existing techniques for monitoring CFGs generate large runtime overhead in real-life applications. This paper demonstrates that monitoring parametric CFGs is practical (with overhead on the order of 12% or lower in most cases). We present a monitor synthesis algorithm for CFGs based on an LR(1) parsing algorithm, modified to account for good prefix matching. In addition, a logic-independent mechanism is introduced to support matching against the suffixes of execution traces. [ABSTRACT FROM AUTHOR]

In this article, we provide an inductive proof system for a notion of abstract non-interference (ANI) which fits in every field of computer science where we are interested in observing how different programs data interfere with each other. The idea is to abstract from language-based security and consider generically data as distinguished between internal (that has to be protected by the program) and observable. In this more general context, we derive a proof system that allows us -to characterize ANI properties inductively on the syntactic structure of programs. We finally show how this framework can be instantiated to language-based security. [ABSTRACT FROM PUBLISHER]

The main objective of this paper is to present an approach to accomplish verification in the early design phases of a system, which allows us to make the system verification easier, specifically for those systems with timing restrictions. For this purpose we use RT-UML sequence diagrams in the design phase and we translate these diagrams into timed automata for performing the verification by using model checking techniques. Specifically, we use the Object Management Group's UML Profile for Schedulability, Performance, and Time and from the specifications written using this profile we obtain the corresponding timed automata. The ‘RT-UML Profile’ is used in conjunction with a very well-known tool to perform validation and verification of the timing needs, namely, the UPPAAL tool, which is used to simulate and analyze the behaviour of real-time dynamic systems described by timed automata. Copyright © 2009 John Wiley & Sons, Ltd. [ABSTRACT FROM AUTHOR]

The three main assertion-based verification approaches are: run-time assertion checking (RAC), extended static checking (ESC) and full formal verification (FFV). Each approach offers a different balance between rigour and ease of use, making them appropriate in different situations. Our goal is to explore the use of these approaches together in a flexible way, enabling an application to be broken down into parts with different reliability requirements and different verification approaches used in each part. We explain the benefits of using the approaches together, present a set of guidelines to avoid potential conflicts and give an overview of how the Omnibus IDE provides support for the full range of assertion-based verification approaches within a single tool. [ABSTRACT FROM AUTHOR]

Natural languages have vast vocabularies, complex grammars and inherent ambiguities that make them difficult to be processed directly by computers, even with state-of-the-art technology. Therefore, in order to communicate with computers we need to 'develop software', which is actually the very process of translating our problem statements, data and solution algorithms from the languages we speak to the languages that computers speak. But software development and maintenance are costly, time consuming and have many major challenges of their own. In this document we present a group of techniques and tools, collectively named as Temizer Description System, that aim to bridge the gap between natural languages and computer languages by enabling computers to understand the logical structure of natural language texts. The main idea is to tag texts piece by piece in order to make them semantically meaningful to the computers. Once computers start figuring out the meaning of text chunks, they can also use the same chunks to talk back to us and we demonstrate how this new and effective way of communication could be used to automate (i.e. eliminate) many tedious and error-prone aspects of developing and maintaining software. [ABSTRACT FROM AUTHOR]

Predicate abstraction has become one of the most successful methodologies for proving safety properties of programs. Recently, several abstraction methodologies have been proposed for proving liveness properties. This paper studies "ranking abstraction" where a program is augmented by a non-constraining progress monitor based on a set of ranking functions, and further abstracted by predicate-abstraction, to allow for automatic verification of progress properties. Unlike many liveness methodologies, the augmentation does not require a complete ranking function that is expected to decrease with each helpful step. Rather, adequate user-provided inputs are component rankings from which a complete ranking function may be automatically formed. The premise of the paper is an analogy between the methods of ranking abstraction and predicate abstraction, one ingredient of which is refinement: When predicate abstraction fails, one can refine it. When ranking abstraction fails, one must determine whether the predicate abstraction, or the ranking abstraction, needs be refined. The paper presents strategies for determining which case is at hand, and methods for performing the apporpriate refinements. The other part of the analogy is that of automatically deriving deductive proof constructs: Predicate abstraction is often used to derive program invariants for proving safety properties as a boolean combination of the given predicates. Deductive proof of progress properties requires well-founded ranking functions in addition to invariants. We show how the constructs necessary for a deductive proof of an arbitrary LTL formula can be automatically extracted from a successful application of the ranking abstraction method. [ABSTRACT FROM AUTHOR]

Previously, we proposed a verification method via invariants for communication protocols modeled as 2-ECFSMs. In the proposed method, a human verifier describes an invariant of a given protocol in a disjunctive normal form and a verification system shows safety or liveness based on the invariant. The tedious work of describing invariant formulae is the most significant shortcoming of the proposed method. This paper deals with semi-automated derivation of invariant formulae for communication protocols modeled as 2-ECFSMs. In the method, the logical formula which holds on a subset of reachable states is automatically generated. Such a subset consists of states which are reachable by synchronous communication from the initial states and those which are reachable by sequences of sending transitions from synchronously reachable states. To obtain an invariant, a human verifier supplements several disjuncts for the other part of the reachability set. We conducted an experiment on deriving an invariant formula for a sample protocol extracted from the OSI session protocol. From the result, 632 conjunctive formulae were automatically derived and the disjunction of those formulae was shown to be an invariant of the sample protocol, i.e. the sample protocol was shown to be safe automatically. © 1998 Scripta Technica. Electron Comm Jpn Pt 1, 81(3): 1–10, 1998 [ABSTRACT FROM AUTHOR]