Incremental Component-based Construction and Verification

Title:Incremental Component-based Construction and Verification
Speaker: Rongjie Yan (晏荣杰)
Time:3:00pm, Thursday, Jan.6
Venue:Lecture Room, Level 3 Building #5, Institute of Software, CAS

Abstract:We propose invariant-based techniques for the efficient verification of safety and deadlock freedom properties of component-based systems. Components and their interactions are described in the BIP language. Global invariants of composite components are obtained by combining local invariants of their constituent components with interaction invariants that take interactions into account.

We study new techniques for computing interaction invariants. Some of these techniques are incremental that is interaction invariants of a composite hierarchically structured component are computed by reusing invariants of its constituents. We formalize incremental construction of components in the BIP language as the process of building progressively complex components by adding interactions (synchronization constraints) to atomic components. We provide sufficient conditions ensuring preservation of invariants when new interactions are added. When these conditions are not satisfied, we propose methods for generating new invariants in an incremental manner. The reuse of existing invariants reduces considerably the overall verification effort.

The techniques have been implemented in the D-Finder toolset. Among the experiments conducted, we have been capable of verifying properties and deadlock-freedom of subsystems of the functional level of the DALA autonomous robot consisting of 500000 lines of C code. This work in collaboration with industrial partners, is far beyond the capacity of existing verification tools.
Bio:
Rongjie Yan received her Ph.D. degree from Institute of Software, Chinese Academy of Sciences in 2007. She has been a postdoctoral researcher in Verimag, France for two years. Her research interests include formal verification and temporal logic. Recently, her research interest focuses on compositional and incremental verification methodology, and correctness-by-construction of component-based systems.