The rely-guarantee approach is a promising way for compositional verification of concurrent reactive systems (CRSs), e.g. concurrent operating systems, interrupt-driven control systems and business process systems. However, various reaction patterns, different abstraction levels of specification, and the complexity of real-world CRSs are still challenging the rely-guarantee approach. PiCore is a rely-guarantee reasoning framework for formal specification and verification of CRSs. We design an event specification language supporting complex reaction structures and its rely-guarantee proof system to detach specification and logic of reactive aspects of CRSs from event behaviours. PiCore parametrizes the language and its rely-guarantee system for event behavior using a rely-guarantee interface and allows to easily integrate 3rd-party languages (CSimpl and Isabelle Hoare_Parallel) via a rely-guarantee adapter. By this design, we have successfully integrated two existing languages and their rely-guarantee proof systems without any change of their specification and proofs. PiCore has been applied to two real-world case studies, i.e. formal verification of concurrent memory management in Zephyr RTOS and a verified translation for a standardized Business Process Execution Language (BPEL) to PiCore.

We have applied PiCore to the formal specification and mechanized proof of the concurrent buddy memory allocation of Zephyr RTOS released by the Linux Foundation. The formal specification is fine-grained providing a high level of detail. It closely follows the Zephyr C code, covering all the data structures and imperative statements present in the implementation. We use the rely-guarantee proof system of PiCore for the formal verification of functional correctness and invariant preservation in the model, revealing three bugs in the C code.

We have also developed a rely-guarantee reasoning approach for asynchronous messaging systems for autonomous vehicles. The axiom model of messaging systems by extending PiCore, which is reusable for concrete applications. The model supports dynamic configuration of message buffers as well as the automatic generation of the rely and guarantee conditions for compositional reasoning.By this approach, we formally verify the DGPS (Differential Global Positioning System) of UISEE autonomous driving systems. The specification and its proof provide a strong evidence for the ongoing safety certification of DGPS.

Scalable and automatic formal verification for concurrent systems is always demanding. In this paper, we propose a verification framework to support automated compositional reasoning for concurrent programs with shared variables. Our framework models concurrent programs as succinct automata and supports the verification of multiple important properties. Safety verification and simulations of succinct automata are parallel compositional, and safety properties of succinct automata are preserved under refinements. We generate succinct automata from infinite state concurrent programs in an automated manner. Furthermore, we propose the first automated approach to checking rely-guarantee based simulations between infinite state concurrent programs. We have prototyped our algorithms and applied our tool to the verification of multiple refinements.

• Fuyuan Zhang, Yongwang Zhao, David Sanan, Yang Liu, Alwen Tiu, Shang-wei Lin, Jun Sun, "Compositional Reasoning for Shared-variable Concurrent Programs", 22nd International Symposium on Formal Methods (FM 2018), 15-17 July 2018, Oxford UK, pp. 523-541 (CCF B, Top conf. in formal methods) [PDF download]

Assurance of information-flow security by formal methods is mandated in security certification of critical software, such as OS kernels. We develop in Isabelle/HOL a generic information-flow security model covering Noninterference, Noninfluence, Nonleakage, and their variants. An logical inference framework shows the precise relation of the security properties. We propose a stepwise refinement approach preserving the security properties at abstract level to concrete level. Finally, six flaws about information-flow security, which can cause information leakage, are found in the ARINC 653 standard and operating systems (VxWorks 653, POK, and XtratuM).

Then we extend our framework to capability-based systems with dynamic policies. We formally specify and verify a capability-based system model with dynamic information flow policies. The system model for capability-based secure systems. The system model specifies critical events including system initialization, inter-domain communication, and capability management. We prove information flow security of the capability-based model by an unwinding theorem. Formal specification and security proof are carried out in the Isabelle/HOL theorem prover and could be applied to formally develop and verify the security of capability-based secure systems, such as separation kernels and secure hypervisors. To our knowledge, this is the first machine-checked proof of capability-based information security with dynamic policies.

The quality and correct functioning of software systems are of prime concern. In addition to classical testing techniques, formal techniques like model checking are used to reinforce the reliability of software systems. However, obtaining of behavior model, which is essential for model-based techniques, of unknown software systems is a challenging task. To mitigate this problem, an emerging black-box analysis technique, called Model Learning, can be applied. We routinely manage to learn the behavior of a device or computer program by just pressing buttons and observing the resulting behavior. Especially children are very good at this and know exactly how to use a smartphone or microwave oven without ever consulting a manual. In such situations, we construct a mental model or state diagram of the device: through experiments we determine in which global states the device can be and which state transitions and outputs occur in response to which inputs.

Our paper is the first survey in this research field. We comprehensively review the background and foundations, well-known tools and successful applications of model learning. We also propose an approach that combines the strengths of two effective techniques, i.e., Model learning and Model checking for the formal analysis of Java libraries.