OVADO²® est un outil RATP qualifié et extensible, dédié à la validation formelle des données de configuration des logiciels et systèmes. L’article Generating and verifying configuration data with OVADO²® décrit une utilisation d’OVADO²® dans le cadre d’un projet SIL4 de génération formelle de données de configuration.
Dans le cadre de certains portages Ada, on peut souhaiter continuer à faire vivre un temps le code legacy tout en commençant à utiliser le code porté.
Si, à l’issue du portage, on découvre un problème ou une évolution dans le code legacy, on devra alors reporter les modifications induites dans le code porté. On peut aussi avoir la situation inverse. En d’autres termes, les codes devront coexister.
Dans la littérature, on trouve une taxinomie des bugs teintée d’humour, mais non dépourvue d’une certaine réalité.
Pour assurer un certain nombre de services au sein de votre application Ada, il peut être intéressant et élégant d’utiliser des applications déjà existantes. Par exemple, si je dois faire des requêtes FTP, il est évidemment plus simple d’utiliser le client du même nom. Si l’application que vous voulez utiliser est en mode interactif (c’est le cas de la commande ftp) alors, la tâche risque d’être ardue.
In the Industry 4.0 context, data are a valuable asset that must be protected. OPC UA PubSub enables secure and interoperable solutions, but authentication of IIoT devices remains a sensitive issue. This article presents a novel approach based on open source software, using a Trusted Platform Module to protect secrets on devices, and evaluate the security level on a predictive maintenance use case.
The OVADO²®1 tool has been used for more than a decade to formally check whether system configuration data comply with their rules in the context of railway systems2. OVADO²® is currently deployed in SIL4 processes compliant with the safety requirements of the CENELEC EN 50128 standard. In these processes, it is considered a T2-class tool since it only helps to verify the system. This article describes how the OVADO²® tool has been used, for the first time, by Systerel to formally generate equipment configuration data derived from the system configuration data.
Formal methods to control the compliance of software implementations
Back-to-back testing (B2BT) techniques are used to verify that two products of a software development process are equivalent. By running the two products “back to back” on a set of test cases, it is verified that they produce the same output. If the scenarios are chosen carefully and the two runs produce the same results, it can be inferred that the two products are equivalent with some level of confidence.
Dans le cadre d’un projet réalisé pour l’un de ses clients, Systerel a dû trouver et mettre en œuvre une solution permettant d’intégrer au sein d’une application Ada2012 un mécanisme permettant de modifier simplement et à la volée le comportement de cette dernière sans avoir à modifier et donc à recompiler le code Ada2012 mis en œuvre.
Dans la phase de construction ou de rénovation de bâtiments, un soin tout particulier doit être apporté à la mise en place d’échafaudages. Ces derniers permettent un accès au chantier efficace et sûr pour les artisans et le matériel.
Pour le développement d’une application, c’est exactement la même chose, votre échafaudage sera ici l’environnement de développement.
Au travers de l’article Démarche de portage d’un “legacy” Ada nous avions présenté les principaux problèmes pouvant être rencontrés lors d’un portage d’un legacy Ada et la façon de les adresser au mieux. L’approche ainsi proposée était « classique » et elle ne faisait aucunement appel aux méthodes formelles au travers par exemple de la technologie SPARK.
Dans le présent article, nous allons vous présenter en quoi la technologie SPARK peut conforter cette approche « classique ».
