Formal Architecture Modeling of Sequential C-Programs
2016 (English)In: Formal Aspects of Component Software: 11th International Symposium, FACS 2014, Bertinoro, Italy, September 10-12, 2014, Revised Selected Papers, Springer, 2016, 312-329- p.Conference paper (Refereed)
To enable verification of a complex C-program, so called compositional verification can be used where the specification for the C-program is split into a set of specifications organized such that the fact that the C-program satisfies its specification can be inferred from verifying that parts of the C-program satisfy their specifications. To support the approach in practice, specifications must be organized in parallel to a formal architecture model capturing the C-program as a hierarchical structure of components with well-defined interfaces. Previous modeling approaches lack support for formal architecture modeling of C-programs. Therefore, a general and formal approach for architecture modeling of sequential C-programs is presented, to support compositional verification, as well as to aid design and management of such C-programs in general.
Place, publisher, year, edition, pages
Springer, 2016. 312-329- p.
Engineering and Technology Mechanical Engineering Mathematics
IdentifiersURN: urn:nbn:se:kth:diva-177634DOI: 10.1007/978-3-319-28934-2_17ScopusID: 2-s2.0-84958074657OAI: oai:DiVA.org:kth-177634DiVA: diva2:873800
12th International Conference on Formal Aspects of Component Software (FACS'15)
QC 2016-02-112015-11-252015-11-252016-05-31Bibliographically approved