Visible to the public Dependence Analysis and Automated Partitioning for Scalable Formal Analysis of SystemC Designs

TitleDependence Analysis and Automated Partitioning for Scalable Formal Analysis of SystemC Designs
Publication TypeConference Paper
Year of Publication2020
AuthorsHerber, Paula, Liebrenz, Timm
Conference Name2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)
Date Publisheddec
KeywordsBrakes, compositionality, Hardware, Predictive Metrics, process control, pubcrawl, Resiliency, Scalability, scalable verification, Sensors, Software, Timing, Wheels
AbstractEmbedded systems often consist of deeply intertwined hardware and software components. At the same time, they are often used in safety-critical applications, where an error may result in enormous costs or even loss of human lives. Existing verification techniques that show the absence of errors do not scale well for complex integrated HW/SW systems. In this paper, we present a dependence analysis and automated partitioning approach for the formal analysis of HW/SW codesigns that are modeled in SystemC. The key idea of our approach is threefold: first, we partition a given system into loosely coupled submodels. Second, we analyze the dependences between these submodels and compute an abstract verification interface for each of them, which captures all possible influences of all other submodels. Third, we verify global properties of the overall system by verifying them separately for each subsystem. We demonstrate that our approach significantly reduces verification times and increases scalability with results for an anti-lock braking system.
Citation Keyherber_dependence_2020