research-article

Mechanizing AADL in Coq - Extended Abstract

Author:

J. HuguesAuthors Info & Claims

ACM SIGAda Ada Letters, Volume 44, Issue 1

Pages 43 - 46

https://doi.org/10.1145/3706601.3706606

Published: 02 December 2024 Publication History

Get Access

Abstract

In this extended abstract, we present a mechanization of the SAE AADL language using Coq along with specific analysis capabilities. Our contribution provides an unambiguous semantics for a large set of the language and can be used as a foundation to build rich analysis capabilities. Our contribution differs from typical language mechanization, it provides support for manipulating modeling constructs, perform verification - ranging from syntactic and semantics checks to formal verification of key properties, and support simulation capabilities.

References

[1]

Y. Bertot and P. Castéran, Interactive theorem proving and program development - Coq-Art: The calculus of inductive constructions. Texts in theoretical computer science. An EATCS series, Springer, 2004.

Crossref

Google Scholar

[2]

B. C. Pierce, A. Azevedo de Amorim, C. Casinghino, M. Gaboardi, M. Greenberg, C. Hri¸tcu, V. Sjöberg, and B. Yorgey, Logical Foundations. Software Foundations series, volume 1, Electronic textbook, May 2018.

Google Scholar

[3]

C. Pit-Claudel and T. Bourgeat, "An experience report on writing usable DSLs in Coq," 2021.

Google Scholar

[4]

J. Hugues, B. Zalila, L. Pautet, and F. Kordon, "From the prototype to the final embedded system using the ocarina AADL tool suite," ACM Trans. Embed. Comput. Syst., vol. 7, no. 4, pp. 42:1--42:25, 2008.

Digital Library

Google Scholar

Index Terms

Mechanizing AADL in Coq - Extended Abstract
1. Software and its engineering
  1. Software notations and tools
2. Theory of computation
  1. Formal languages and automata theory
  2. Semantics and reasoning
    1. Program semantics

Index terms have been assigned to the content through auto-classification.

Recommendations

Completeness and decidability of converse PDL in the constructive type theory of Coq
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs

The completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof ...
A Coq Mechanization of JavaScript Regular Expression Semantics

We present an executable, proven-safe, faithful, and future-proof Coq mechanization of JavaScript regular expression (regex) matching, as specified by the latest published edition of ECMA-262 section 22.2. This is, to our knowledge, the first time that ...
Call-by-push-value in Coq: operational, equational, and denotational theory
CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

Call-by-push-value (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both call-by-value (CBV) and call-by-name (CBN). We formalise weak and strong operational semantics for (effect-free) ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGAda Ada Letters Volume 44, Issue 1

June 2024

148 pages

DOI:10.1145/3706601

Editor:
Luis Miguel Pinho
Polytechnic Institute of Porto, Porto, Portugal

Issue’s Table of Contents

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 December 2024

Published in SIGADA Volume 44, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

0
Total Citations
10
Total Downloads

Downloads (Last 12 months)10
Downloads (Last 6 weeks)10

Reflects downloads up to 28 Dec 2024

Other Metrics

View Author Metrics

Citations

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Index Terms

Recommendations

Completeness and decidability of converse PDL in the constructive type theory of Coq

A Coq Mechanization of JavaScript Regular Expression Semantics

Call-by-push-value in Coq: operational, equational, and denotational theory