Formal Methods and Software Engineering

Security-oriented analyses of information flow can be in terms of channels (entropy leakage), or in terms of programs (noninterference); and for each we can consider deterministic, demonic or probabilistic instances. We discuss all 2×3 = 6 cases from a common point of view, seeking a uniform approach to a partial order of information. In some cases this is a lattice (as is already known); and in some cases it seems not to be (novel).

This work presents a conservative extension of OhCircus, a concurrent specification language, which integrates CSP, Z, object-orientation and embeds a refinement calculus. This extension supports the definition of process inheritance, where control flow, operations and state components are eligible for reuse. We present the extended OhCircus grammar and, based on Hoare and He’s Unifying Theories of Programming, we give the formal semantics of process inheritance and its supporting constructs. The main contribution of this work is a set of sound algebraic laws for process inheritance. The proposed laws are exercised in the development of a case study.

The UML Profile for Modeling and Analysis of Real-Time and Embedded systems promises a general modeling framework to design and analyze systems. Lots of works have been published on the modeling capabilities offered by MARTE, much less on verification techniques supported. The Clock Constraint Specification Language (CCSL), first introduced as a companion language for MARTE, was devised to offer a formal support to conduct causal and temporal analyses on MARTE models.

This work introduces formally a state-based semantics for CCSL operators and then focuses on the analysis capabilities of MARTE/CCSL and more particularly on boundness issues.

The approach is illustrated on one simple example where the architecture plays an important role. We describe a process where the logical description of the application is progressively refined to take into account the candidate execution platforms through allocation.

Specification mining has become an attractive tool for assisting in numerous software development and maintenance tasks. The majority of these techniques share a common assumption: significant program properties occur frequently. Unfortunately, statistical inference alone produces too many program properties, many of which are found to be either insignificant or meaningless. Consequently, it becomes a laborious task for developers to separate semantically meaningful specifications from the rest. In this paper, we present a semantic-directed specification mining framework that injects in-depth semantics information into mining input. Specifically, we investigate the introduction of dataflow semantics to extract dataflow related sequences from execution traces, and demonstrate that mining specifications from these dataflow related sequences reduces a great number of meaningless specifications, resulting in a collection of specifications which are both semantically relevant and statistically significant. Our experimental results indicate that our approach can effectively filter out insignificant specifications and greatly improve the efficiency of mining. In addition, we also show that our mined specifications reflect the essential program behavior and can practically help program understanding and bug detection.

In the context of program verification, we propose a formal framework for proof slicing that can aggressively reduce the size of proof obligations as a means of performance improvement. In particular, each large proof obligation may be broken down into smaller proofs, for which the overall processing cost can be greatly reduced, and be even more effective under proof caching. Our proposal is built on top of existing automatic provers, including the state-of-the-art prover Z3, and can also be viewed as a re-engineering effort in proof decomposition that attempts to avoid large-sized proofs for which these provers may be particularly inefficient. In our approach, we first develop a calculus that formalizes a complete proof slicing procedure, which is followed by the development of an aggressive proof slicing method. Retaining completeness is important, and thus in our experiments the complete method serves as a backup for the cases when the aggressive procedure fails. The foundations of the aggressive slicing procedure are based on a novel lightweight annotation scheme that captures weak links between sub-formulas of a proof obligation; the annotations can be inferred automatically in practice, and thus both methods are fully automated.

The safety and security of software systems depends on how they are initially configured. Manually writing program code that establishes such an initial configuration is a tedious and error-prone engineering process. In this paper we present an automatic and formally verified initialiser for component-based systems built on the general-purpose microkernel seL4. The construction principles of this tool apply to capability systems in general and the proof ideas are not specific to seL4. The initialiser takes a declarative formal description of the desired initialised state and uses seL4-provided services to create all necessary components, setup their communication channels, and distribute the required access rights. We provide a formal model of the initialiser and prove, in the theorem prover Isabelle/HOL, that the resulting state is the desired one. Our proof formally connects to the existing functional correctness proof of the seL4 microkernel. This tool does not only provide automation, but also unprecedented assurance for reaching a desired system state. In addition to the engineering advantages, this result is a key prerequisite for reasoning about system-wide security and safety properties.

In this paper, we present a verification of an aircraft proximity characterization method in the proof assistant Coq. Our verification covers aircraft kinematics, foundational geometric objects, and real analysis, which are all used in the proximity characterization method. These subjects from different areas make our verification complicated. Through the verification, all proximity characteristics in that method are formalized and provided with machine-checkable proofs. We have identified and corrected several mistakes in the informal description of the method, and improved the accuracy of proximity characteristics by explicitly defining their conditions in the formalization. Our verification shows the effectiveness of using Coq to increase the trust to the aircraft proximity characterization method.

Program invariants play a major role in program analysis, the specification refinement technique has the capability to generating all the required program invariants for verifying a specification. The refinement invariants generation is the main obstacles of the specification refinement. Based on random testing, this paper presents a practical assistant approach for specification refinement. The effectiveness of the approach is demonstrated on examples.

Finite state machine-based testing aims at generating checking sequences that guarantee the conformance between the implementation and the specification of a system. For that purpose, several methods have been proposed to generate checking sequences which ensure full coverage of possible faults in the implementation. Many existing methods are based on a special sequence, called distinguishing sequence, which does not exist for every minimal machine. Some methods are based on characterization sets since they exist for every machine. However, these methods generate checking sequences exponentially long. In this paper, we propose a method to generate checking sequences using identification sets. These sets exist for every minimal FSM and also lead to shorter checking sequences. We conducted an experimental study to compare the proposed method with the existing methods. The results show that on average our method generates checking sequences 31.7% to 99.9% shorter than the ones produced by existing methods.

Formal specifications provide strong bases for testing and bring powerful techniques and technologies. Expressive formal specification languages combine large data domain and behavior. Thus, symbolic methods have raised particular interest for test generation techniques.

Integrating formal testing in proof environments such as Isabelle/HOL is referred to as “theorem-prover based testing”. Theorem-prover based testing can be adapted to a specific specification language via a representation of its formal semantics, paving the way for specific support of its constructs. The main challenge of this approach is to reduce the gap between pen-and-paper semantics and formal mechanized theories.

We discovered unforeseen simplifications in both definitions and symbolic computations. The approach lends itself to the construction of a tool, that directly uses semantic definitions of the language as well as derived rules of its testing theory, and thus provides some powerful symbolic computation machinery to seamlessly implement them both in a technical environment.

Here we propose a timed input-output conformance relation (named CSPTIO) based on the process algebra CSP. In contrast to other relations, CSPTIO analyses data-flow reactive systems and conformance verification is mechanised in terms of a high-level strategy by reusing successful techniques and tools: refinement checking (particularly, using the FDR tool) and SMT solving (using Z3). Therefore, conformance verification does not require the implementation of specific algorithms or the manipulation of complex data structures. Furthermore, the mechanisation is proved sound. To analyse the usefulness of CSPTIO, we first consider a toy example. Then we analyse critical systems from two different domains: aeronautics and automotive. CSPTIO detected all undesired behaviours in the analysed implementation models.

Real-time system verification must deal with a special notion of ‘fairness’, i.e., clocks must always be able to progress. A system run which prevents clocks from progressing unboundedly is known as Zeno. Zeno runs are infeasible in reality and thus must be pruned during system verification. Though zone abstraction is an effective technique for model checking real-time systems, it is known that zone graphs (e.g., those generated from Timed Automata models) are too abstract to directly infer time progress and hence non-Zenoness. As a result, model checking with non-Zenoness (i.e., existence of a non-Zeno counterexample) based on zone graphs only is infeasible. In our previous work [23], we show that model checking Stateful Timed CSP with non-Zenoness based on zone graphs only is feasible, due to the difference between Stateful Timed CSP and Timed Automata. Nonetheless, the algorithm proposed in [23] requires to associate each time process construct with a unique clock, which could enlarge the state space (compared to model checking without non-Zenoness) significantly. In this paper, we improve our previous work by combining the checking algorithm with a clock-symmetry reduction method. The proposed algorithm has been realized in the PAT model checker for model checking LTL properties with non-Zenoness. The experimental results show that the improved algorithm significantly outperforms the previous work.

Over the past two decades, numerous verification tools have been successfully used for verifying complex concurrent systems, modelled using various formalisms. However, it is still hard to coordinate these tools since they rely on such a large number of formalisms. Having a proper syntactical mechanism to interrelate them through variability would increase the capability of effective integrated formal methods. In this paper, we propose a modular approach for defining new formalisms by reusing existing ones and adding new features and/or constraints. Our approach relies on standard XML technologies; their use provides the capability of rapidly and automatically obtaining tools for representing and validating models. It thus enables fast iterations in developing and testing complex formalisms. As a case study, we applied our modular definition approach on families of Petri nets and timed automata.

CSP# (Communicating Sequential Programs) is a modelling language designed for specifying concurrent systems by integrating CSP-like compositional operators with sequential programs updating shared variables. In this paper, we define an observation-oriented denotational semantics in an open environment for the CSP# language based on the UTP framework. To deal with shared variables, we lift traditional event-based traces into hybrid traces which consist of event-state pairs for recording process behaviours. We also define refinement to check process equivalence and present a set of algebraic laws which are established based on our denotational semantics. Our approach thus provides a rigorous means for reasoning about the correctness of CSP# process behaviours. We further derive a closed semantics by focusing on special types of hybrid traces; this closed semantics can be linked with existing CSP# operational semantics.

Mainstream languages such as C/C++ (with Pthreads), Java, and .NET provide programmers with both static and dynamic barriers for synchronizing concurrent threads in fork/join programs. However, such barrier synchronization in fork/join programs is hard to verify since programmers must not only keep track of the dynamic number of participating threads, but also ensure that all participants proceed in correctly synchronized phases. As barriers are commonly used in practice, verifying correct synchronization of barriers can provide compilers and analysers with important phasing information for improving the precision of their analyses and optimizations.

In this paper, we propose an approach for statically verifying correct synchronization of static and dynamic barriers in fork/join programs. We introduce the notions of bounded permissions and phase numbers for keeping track of the number of participating threads and barrier phases respectively. The approach has been proven sound, and a prototype of it (named VeriBSync) has been implemented for verifying barrier synchronization of realistic programs in the SPLASH-2 benchmark suite.

In this paper, we propose a formalisation of SysML blocks based on a state-rich process algebra that supports refinement, namely, CML. We first establish a set of guidelines of usage of SysML block definition and internal block diagrams. Next, we propose a formal semantics of SysML blocks described by diagrams that conform to our guidelines. The semantics is specified by inductive functions over the structure of SysML models. These functions can be mechanised to support automatic generation of the CML models.

The Systems Modeling Language (SysML), an extension of a subset of the Unified Modeling Language (UML), is a visual modelling language for systems engineering applications. At present, the semi-formal SysML, which is widely utilised for the design of complex heterogeneous systems, lacks integration with other more formal approaches. In this paper, we describe how Communicating Sequential Processes (CSP) and its associated refinement checker, Failures Divergence Refinement (FDR), may be used to underpin an approach that facilitates the refinement checking of behavioural consistency of SysML diagrams; we also show how the proposed approach supports requirements traceability. We illustrate our contribution by means of a small case study.

An automatic translation from Workflow nets (WFNs) to Modeling, Simulation and Verification Language (MSVL) is presented in this paper. As a result, WFNs can be simulated and verified through the well developed supporting tool named MSV for MSVL programs. To do so, annotations are added to WFNs first. Further, translating rules are presented w.r.t regular structures for the translation from Annotated WFNs to MSVL programs. Finally, a tool called PN2MSVL has been implemented for the automatic translation from WFNs to MSVL.

The majority of existing probabilistic model checking case studies are based on well understood theoretical models and distributions. However, real-life probabilistic systems usually involve distribution parameters whose values are obtained by empirical measurements and thus are subject to small perturbations. In this paper, we consider perturbation analysis of reachability in the parametric models of these systems (i.e., parametric Markov chains) equipped with the norm of absolute distance. Our main contribution is a method to compute the asymptotic bounds in the form of condition numbers for constrained reachability probabilities against perturbations of the distribution parameters of the system. The adequacy of the method is demonstrated through experiments with the Zeroconf protocol and the hopping frog problem.

Web services have emerged as an important technology nowadays. There are two kinds of requirements that are crucial to web service composition, which are functional and non-functional requirements. Functional requirements focus on functionality of the composed service, e.g., given a booking service, an example of functional requirements is that a flight ticket with price higher than $2000 will never be purchased. Non-functional requirements are concerned with the quality of service (QoS), e.g., an example of the booking service’s non-functional requirements is that the service will respond to the user within 5 seconds. Non-functional requirements are important to web service composition, and are often an important clause in service-level agreements (SLAs). Even though the functional requirements are satisfied, a slow or unreliable service may still not be adopted. In our paper, we propose an automated approach to verify combined functional and non-functional requirements directly based on the semantics of web service composition. Our approach has been implemented and evaluated on the real-world case studies, which demonstrate the effectiveness of our method.

Virtualization is widely used for critical services like Cloud computing. It is desirable to formally verify virtualization systems. However, the complexity of the virtualization system makes the formal analysis a difficult task, e.g., sophisticated programs to manipulate low-level technologies, paged memory management, memory mapped I/O and trusted computing. In this paper, we propose a formal framework, vTRUST, to formally describe virtualization systems with a carefully designed abstraction. vTRUST includes a library to model configurable hardware components and technologies commonly used in virtualization. The system designer can thus verify virtualization systems on critical properties (e.g., confidentiality, verifiability, isolation and PCR consistency) with respect to certain adversary models. We demonstrate the effectiveness of vTRUST by automatically verifying a real-world Cloud implementation with critical bugs identified.

Kinematic analysis is used for trajectory planning of robotic manipulators and is an integral step of their design. The main idea behind kinematic analysis is to study the motion of the robot based on the geometrical relationship of the robotic links and their joints. Given the continuous nature of kinematic analysis, traditional computer-based verification methods, such as simulation, numerical methods or model checking, fail to provide reliable results. This fact makes robotic designs error prone, which may lead to disastrous consequences given the safety-critical nature of robotic applications. Leveraging upon the high expressiveness of higher-order logic, we propose to use higher-order-logic theorem proving for conducting formal kinematic analysis. As a first step towards this direction, we utilize the geometry theory of HOL-Light to develop formal reasoning support for the kinematic analysis of a two-link planar manipulator, which forms the basis for many mechanical structures in robotics. To illustrate the usefulness of our foundational formalization, we present the formal kinematic analysis of a biped walking robot.

Reliable and highly performant handling of large data stores constitutes one of the major challenges of cloud computing. In this paper, we propose a formalisation of a cloud solution implemented by F-Secure – a provider of secure data storage services. The solution is based on massive replication and the write-ahead logging mechanism. To achieve high performance, the company has abandoned a transactional model. We formally derive a model of the proposed architectural solution and verify data integrity and consistency properties under possible failure scenarios. The proposed approach allows the designers to formally define and verify essential characteristics of architectures for handling large data stores.

Wireless technology has achieved lots of applications in computer networks. To model and analyze wireless systems, a calculus called CWS and its operational semantics have been investigated. This paper considers the linking between the algebraic semantics and the operational semantics for this calculus. Our approach is to derive the operational semantics from the algebraic semantics. Firstly we present the algebraic semantics and introduce the concept of head normal form. Secondly we present the strategy of deriving the operational semantics from the algebraic semantics. Based on the strategy, an operational semantics is derived, which shows that the operational semantics is sound with respect to the algebraic semantics. Then the equivalence between the derivation strategy and the derived transition system is proved. This shows the completeness of the derived operational semantics. Finally, we investigate the mechanical approach to our linking method using the equational and rewriting logic system Maude. We mechanize the algebraic laws, the derivation strategy and the derived operational semantics.

Automated discovery of specifications for heap-manipulating programs is a challenging task due to the complexity of aliasing and mutability of data structures. This task is further complicated by an expressive domain that combines shape, numerical and bag information. In this paper, we propose a compositional analysis framework in the presence of user-defined predicates, which would derive the summary for each method in the expressive abstract domain, independently from its callers. We propose a novel abstraction method with a bi-abduction technique in the combined domain to discover pre-/post-conditions that could not be automatically inferred before. The analysis does not only prove the memory safety properties, but also finds relationships between pure and shape domains towards full functional correctness of programs. A prototype of the framework has been implemented and initial experiments have shown that our approach can discover interesting properties for non-trivial programs.

Infeasible code has proved to be an interesting target for static analysis. It allows modular and scalable analysis, and at the same time, can be implemented with a close-to-zero rate of false warnings. The challenge for an infeasible code detection algorithm is to find executions that cover all statements with feasible executions as fast as possible. The remaining statements are infeasible code. In this paper we propose a new encoding of programs into first-order logic formulas that allows us to query the non-existence of feasible executions of a program, and, to reconstruct a feasible path from counterexamples produced for this query. We use these paths to develop a path-cover algorithm based on blocking clauses. We evaluate our approach using several real-world applications and show that our new prover-friendly encoding yields a significant speed-up over existing approaches.

Computer Games Software deeply relies on physics simulations, which are particularly demanding to analyze because they manipulate a large amount of interleaving floating point variables. Therefore, this application domain is an interesting workbench to stress the trade-off between accuracy and efficiency of abstract domains for static analysis.

In this paper, we introduce Parametric Hypercubes, a novel disjunctive non-relational abstract domain. Its main features are: (i) it combines the low computational cost of operations on (selected) multidimensional intervals with the accuracy provided by lifting to a power-set disjunctive domain, (ii) the compact representation of its elements allows to limit the space complexity of the analysis, and (iii) the parametric nature of the domain provides a way to tune the accuracy/efficiency of the analysis by just setting the widths of the hypercubes sides.

The first experimental results on a representative Computer Games case study outline both the efficiency and the precision of the proposal.