2021/03/25 by Miel Sharf, Bart Besselink, Sharf, Miel +3
Computer Science · Engineering · #FOS: Electrical engineering #Formal Methods in Verification #Safety Systems Engineering in Autonomy #Software Reliability and Analysis Research #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.2103.13743
openalex publication_date 2021/03/25 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
Verifying specifications for large-scale modern engineering systems can be a\ntime-consuming task, as most formal verification methods are limited to systems\nof modest size. Recently, contract-based design and verification has been\nproposed as a modular framework for specifications, and\nlinear-programming-based techniques have been presented for verifying that a\ngiven system satisfies a given contract. In this paper, we extend this\nassume/guarantee framework by presenting necessary and sufficient conditions\nfor a collection of contracts on individual components to refine a contract on\nthe composed system. These conditions can be verified by solving linear\nprograms, whose number grows linearly with the number of specifications defined\nby the contracts. We exemplify the tools developed using a case study\nconsidering safety in a car-following scenario, where noise and time-varying\ndelay are considered.\n