Home > Research > Publications & Outputs > On systematic design of globally consistent exe...


Text available via DOI:

View graph of relations

On systematic design of globally consistent executable assertions in embedded software

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Publication date19/06/2002
Host publicationProceedings of the joint conference on Languages, compilers and tools for embedded systems: software and compilers for embedded systems
Number of pages10
ISBN (print)1581135270
<mark>Original language</mark>English


Over the design of software (SW) used in provisioning of dependable services, Executable Assertions (EAs) are seeing increasing usage in aiding detection of data errors. Given the requirements for provision of service despite faults, early detection of system states that can potentially lead to system failure is valuable. We address the issue of ascertaining whether localized EAs in individual modules add up complementarily to implement a global EA/property. We first show that detection of globally compliant EAs is NP-complete. Thus, we develop a two-pass approach for our objective. In the first pass, we introduce the consistency property of EAs and use it to ascertain global conformity across all EAs. The second pass, analogous to predicate transformers, generates globally consistent EAs when any inconsistency is flagged in the first pass. We show the applicability of our approach on a real embedded system. Initial results obtained show that our framework is able to detect inherent vulnerabilities (due to placement of mismatched EAs) that were previously undetected. Our intent is automation of this approach, which can be incorporated in a compiler.