Runtime Verification for Biochemical Programs

Abstract : The biochemical paradigm is well-suited for modelling autonomous systems and new programming languages are emerging from this approach. However, in order to validate such programs, we need to define precisely their semantics and to provide verification techniques. In this paper, we consider a higher-order biochemical calculus that models the structure of system states and its dynamics thanks to rewriting abstractions, namely rules and strategies. We extend this calculus with a runtime verification technique in order to perform automatic discovery of property satisfaction failure. The property specification language is a subclass of LTL safety and liveness properties.
Type de document :
Article dans une revue
Electronic Notes in Theoretical Computer Science, Elsevier, 2013, Proceedings of the first workshop on Hybrid Autonomous Systems, 297, pp.27-46. 〈http://authors.elsevier.com/sd/article/S1571066113000832〉. 〈10.1016/j.entcs.2013.12.003〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00986676
Contributeur : Helene Kirchner <>
Soumis le : samedi 3 mai 2014 - 19:48:32
Dernière modification le : mardi 13 décembre 2016 - 15:40:57

Lien texte intégral

Identifiants

Collections

Citation

Helene Kirchner. Runtime Verification for Biochemical Programs. Electronic Notes in Theoretical Computer Science, Elsevier, 2013, Proceedings of the first workshop on Hybrid Autonomous Systems, 297, pp.27-46. 〈http://authors.elsevier.com/sd/article/S1571066113000832〉. 〈10.1016/j.entcs.2013.12.003〉. 〈hal-00986676〉

Partager

Métriques

Consultations de la notice

127