SyLVaaS: System Level Formal Verification as a Service

摘要: The goal of System Level Formal Verification is to show system correctness notwithstanding uncontrollable events (disturbances), as for example faults, variation in parameters, external inputs, etc. This may be achieved with an exhaustive Hardware In the Loop Simulation based approach, by considering all relevant scenarios Under (SUV) operational environment. this paper, we present SyLVaaS, a Web-based tool enabling Service (VaaS). SyLVaaS implements assume-guarantee approach verification problem outlined above. takes input high-level model defining SUV environment and computes, using parallel algorithms deployed cluster infrastructure, set highly optimised simulation campaigns, which can executed embarrassingly fashion on Simulink instances, platform independent driver downloadable from Web site. As actual carried out at user premises (e.g., private cluster), allows full Intellectual Property protection flow. campaigns computed randomise order enables, anytime during activity, estimation completion time computation upper bound Omission Probability, i.e., probability that there yet-to-be-simulated scenario violates property under verification. information supports graceful degradation activity. We effectiveness infrastructure evaluating industry-scale related Fuel Control (FCS) distribution.