%0 Conference Proceedings
%T Painless Support for Static and Runtime Verification of Component-Based Applications
%+ Safe Composition of Autonomous applications with Large-SCALE Execution environment (SCALE)
%+ Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S)
%+ ActiveEon
%A Gaspar, Nuno
%A Henrio, Ludovic
%A Madelaine, Eric
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 6th Fundamentals of Software Engineering (FSEN)
%C Tehran, Iran
%Y Mehdi Dastani
%Y Marjan Sirjani
%I Springer
%3 Fundamentals of Software Engineering
%V LNCS-9392
%P 259-274
%8 2015-04-22
%D 2015
%R 10.1007/978-3-319-24644-4_18
%K The Coq Proof Assistant
%K Component-based Engineering
%K Formal Methods
%K Architecture Description Language
%Z Computer Science [cs]Conference papers
%X Architecture Description Languages (ADL) provide descriptions of a software system in terms of its structure. Such descriptions give a high-level overview and come from the need to cope with arbitrarily complex dependencies arising from software components.In this paper we present Painless, a novel ADL with a declarative trait supporting parametrized specifications and architectural reconfigurations. Moreover, we exhibit its reliable facet on its integration with ProActive — a middleware for distributed programming. This is achieved by building on top of Mefresa, a Coq framework for the reasoning on software architectures. We inherit its strong guarantees by extracting certified code, and subsequently integrating it in our toolchain.
%G English
%Z TC 2
%Z WG 2.2
%2 https://inria.hal.science/hal-01168757v2/document
%2 https://inria.hal.science/hal-01168757v2/file/978-3-319-24644-4_18_Chapter.pdf
%L hal-01168757
%U https://inria.hal.science/hal-01168757
%~ UNICE
%~ CNRS
%~ INRIA
%~ INRIA-SOPHIA
%~ I3S
%~ INRIASO
%~ INRIA_TEST
%~ TESTALAIN1
%~ IFIP-LNCS
%~ IFIP
%~ INRIA2
%~ IFIP-TC
%~ IFIP-TC2
%~ IFIP-WG2-2
%~ IFIP-LNCS-9392
%~ IFIP-FSEN
%~ UNIV-COTEDAZUR