SAT–Based Bounded Strong Satisfiability Checking of Reactive System Specifications

Abstract : Many fatal accidents involving safety-critical reactive systems have occurred in unexpected situations that were not considered during the design and test phases of the systems. To prevent these accidents, reactive systems should be designed to respond appropriately to any request from an environment at any time. Verifying this property during the specification phase reduces development reworking. This property of a specification is commonly known as realizability. Realizability checking for reactive system specifications involves complex and intricate analysis. For the purpose of detecting simple and typical defects in specifications, we introduce the notion of bounded strong satisfiability (a necessary condition for realizability), and present a method for checking this property. Bounded strong satisfiability is the property that for all input patterns represented by loop structures of a given size k, there is a response that satisfies a given specification. We present a checking method based on a satisfiability solver, and report experimental results.
Type de document :
Communication dans un congrès
David Hutchison; Takeo Kanade; Madhu Sudan; Demetri Terzopoulos; Doug Tygar; Moshe Y. Vardi; Gerhard Weikum; Khabib Mustofa; Erich J. Neuhold; A Min Tjoa; Edgar Weippl; Ilsun You; Josef Kittler; Jon M. Kleinberg; Friedemann Mattern; John C. Mitchell; Moni Naor; Oscar Nierstrasz; C. Pandu Rangan; Bernhard Steffen. 1st International Conference on Information and Communication Technology (ICT-EurAsia), Mar 2013, Yogyakarta, Indonesia. Springer, Lecture Notes in Computer Science, LNCS-7804, pp.60-70, 2013, Information and Communicatiaon Technology. 〈10.1007/978-3-642-36818-9_7〉
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01480266
Contributeur : Hal Ifip <>
Soumis le : mercredi 1 mars 2017 - 11:33:58
Dernière modification le : mercredi 1 mars 2017 - 11:36:36
Document(s) archivé(s) le : mardi 30 mai 2017 - 16:01:01

Fichier

978-3-642-36818-9_7_Chapter.pd...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki. SAT–Based Bounded Strong Satisfiability Checking of Reactive System Specifications. David Hutchison; Takeo Kanade; Madhu Sudan; Demetri Terzopoulos; Doug Tygar; Moshe Y. Vardi; Gerhard Weikum; Khabib Mustofa; Erich J. Neuhold; A Min Tjoa; Edgar Weippl; Ilsun You; Josef Kittler; Jon M. Kleinberg; Friedemann Mattern; John C. Mitchell; Moni Naor; Oscar Nierstrasz; C. Pandu Rangan; Bernhard Steffen. 1st International Conference on Information and Communication Technology (ICT-EurAsia), Mar 2013, Yogyakarta, Indonesia. Springer, Lecture Notes in Computer Science, LNCS-7804, pp.60-70, 2013, Information and Communicatiaon Technology. 〈10.1007/978-3-642-36818-9_7〉. 〈hal-01480266〉

Partager

Métriques

Consultations de la notice

34

Téléchargements de fichiers

22