test_moissonnage_selune
type: Agent

Modern languages for modeling and verifying asynchronous systems
type: Distribution
access URL: https://theses.hal.science/tel-00685209
format: HTML
issued: 2026-05-22T17:53:50.865695
modified: 2026-05-22T17:53:50.770106

Modern languages for modeling and verifying asynchronous systems
type: Dataset
contact point: Organization
  fn: CCSD
keyword: bpel
keyword: langages-modernes-modelisation
keyword: systemes-asynchrones
keyword: theses
keyword: asynchronous-systems
keyword: infoinfo-ohcomputer-science-csother-csoh
keyword: verification-formelle
keyword: infoeu-reposemanticsdoctoralthesis
keyword: meta-modelisation
keyword: lotos-nt
keyword: meta-modelling
keyword: modern-modeling-languages
keyword: formal-verification
landing page: https://theses.hal.science/tel-00685209
description: The work in this thesis is at the intersection of two major research domains~: Model-Driven Engineering (MDE) and formal methods, and has various fields of application. This thesis deals with the formal verification of parallel applications modelled by the MDE approach. In this approach, models play a central role and enable to develop an application through successive transformations (automated or not) between intermediate models of differing levels of abstraction, until executable code is produced. When models have a formal semantics, the application can be verified, either automatically or semi-automatically. These principles are used in TOPCASED, an ECLIPSE-based development environment for critical embedded applications, which enables formal verification by interconnecting existing tools. This thesis implements the TOPCASED approach by relying on the CADP toolbox for verifying systems, and on its most recent input formalism : LOTOS NT. This thesis tackles the formal verification of MDE applications through two real problems : 1) For GALS (Globally Asynchronous, Locally Synchronous), a generic verification method, based on a transformation to LOTOS NT, is proposed and illustrated by an industrial case-study provided by AIRBUS : a communication protocol between the airplane and the ground described in the synchronous langage SAM designed at AIRBUS. 2) For Web services specified with the BPEL (Business Process Execution Language) norm, a verification method is proposed. It is based on a BPEL to LOTOS NT transformation which takes into account XML Schema, Xpath, and WSDL, the languages on which the BPEL norm is built.
identifier: NNT: 2011GRENMO12
issued: 2026-05-22T17:53:50.805235
language: fr
modified: 2026-05-22T17:53:50.805241