Leveraging Compositional Methods for Modeling and Verification of an Autonomous Taxi System
We apply a compositional formal modeling and verification method to an autonomous aircraft taxi system. We provide insights into the modeling approach and we identify several research areas where further development is needed. Specifically, we identify the following needs: (1) semantics of composition of viewpoints expressed in different specification languages, and tools to reason about heterogeneous declarative models; (2) libraries of formal models for autonomous systems to speed up modeling and enable efficient reasoning; (3) methods to lift verification results generated by automated reasoning tools to the specification level; (4) probabilistic contract frameworks to reason about imperfect implementations; (5) standard high-level functional architectures for autonomous systems; and (6) a theory of higher-order contracts. We believe that addressing these research needs, among others, could improve the adoption of formal methods in the design of autonomous systems including learning-enabled systems, and increase confidence in their safe operations.
Code (1)
Similar Papers 제목 키워드 기반
Scenario-based Compositional Verification of Autonomous Systems with Neural Perception
Recent advances in deep learning have enabled the development of autonomous systems that use deep neural networks for perception. Formal verification of these systems is challenging due to the size and complexity of the …
ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
Full verification of learning-enabled cyber-physical systems (CPS) has long been intractable due to challenges including black-box components and complex real-world environments. Existing tools either provide formal guar…
Compositional Verification for Autonomous Systems with Deep Learning Components
As autonomy becomes prevalent in many applications, ranging from recommendation systems to fully autonomous vehicles, there is an increased need to provide safety guarantees for such systems. The problem is difficult, as…
Autonomous VehiclesDeep LearningRecommendation SystemsVerification of Visual Controllers via Compositional Geometric Transformations
Perception-based neural network controllers are increasingly used in autonomous systems that rely on visual inputs to operate in the real world. Ensuring the safety of such systems under uncertainty is challenging. Exist…
Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems
The integration of neural networks into safety-critical systems has shown great potential in recent years. However, the challenge of effectively verifying the safety of Neural Network Controlled Systems (NNCS) persists. …