Rigorous system design flow for autonomous systems

Abstract

We currently lack rigorous approaches for modeling and implementing complex systems. BIP (Behavior, Interaction, Priority) is a component-based framework intended to rigorous system design. It relies on single semantic model for system descriptions all along the design flow. It also includes methods and tools for guaranteeing system correctness to avoid a posteriori verification. Our approach is to check safety properties (e.g. deadlock freedom) at design time using D-Finder verification tool. In addition, source-to-source transformers allow progressive refinement of the application to generate a correct implementation. Our framework was successfully applied in various context including robotics case studies presented here.