Proof-based verification approaches for dynamic properties: application to the information system domain
| LEADER | caa a22 4500 | ||
|---|---|---|---|
| 001 | 605516421 | ||
| 003 | CHVBK | ||
| 005 | 20210128100714.0 | ||
| 007 | cr unu---uuuuu | ||
| 008 | 210128e20150301xx s 000 0 eng | ||
| 024 | 7 | 0 | |a 10.1007/s00165-014-0323-x |2 doi |
| 035 | |a (NATIONALLICENCE)springer-10.1007/s00165-014-0323-x | ||
| 245 | 0 | 0 | |a Proof-based verification approaches for dynamic properties: application to the information system domain |h [Elektronische Daten] |c [Amel Mammar, Marc Frappier] |
| 520 | 3 | |a This paper proposes a formal approach for generating necessary and sufficient proof obligations to demonstrate a set of dynamic properties using the B method. In particular, we consider reachability, non-interference and absence properties. Also, we show that these properties permit a wide range of property patterns introduced by Dwyer to be expressed. An overview of a tool supporting these approaches is also provided. | |
| 540 | |a British Computer Society, 2014 | ||
| 690 | 7 | |a Dynamic properties |2 nationallicence | |
| 690 | 7 | |a B formal method |2 nationallicence | |
| 690 | 7 | |a Proof |2 nationallicence | |
| 690 | 7 | |a Property patterns |2 nationallicence | |
| 700 | 1 | |a Mammar |D Amel |u Institut Telecom/Telecom SudParis, CNRS/SAMOVAR, Évry, France |4 aut | |
| 700 | 1 | |a Frappier |D Marc |u GRIL, Département d'informatique, Université de Sherbrooke, 2500 Boulevard Université, J1K 2R1, Sherbrooke, QC, Canada |4 aut | |
| 773 | 0 | |t Formal Aspects of Computing |d Springer London |g 27/2(2015-03-01), 335-374 |x 0934-5043 |q 27:2<335 |1 2015 |2 27 |o 165 | |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s00165-014-0323-x |q text/html |z Onlinezugriff via DOI |
| 898 | |a BK010053 |b XK010053 |c XK010000 | ||
| 900 | 7 | |a Metadata rights reserved |b Springer special CC-BY-NC licence |2 nationallicence | |
| 908 | |D 1 |a research-article |2 jats | ||
| 949 | |B NATIONALLICENCE |F NATIONALLICENCE |b NL-springer | ||
| 950 | |B NATIONALLICENCE |P 856 |E 40 |u https://doi.org/10.1007/s00165-014-0323-x |q text/html |z Onlinezugriff via DOI | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Mammar |D Amel |u Institut Telecom/Telecom SudParis, CNRS/SAMOVAR, Évry, France |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Frappier |D Marc |u GRIL, Département d'informatique, Université de Sherbrooke, 2500 Boulevard Université, J1K 2R1, Sherbrooke, QC, Canada |4 aut | ||
| 950 | |B NATIONALLICENCE |P 773 |E 0- |t Formal Aspects of Computing |d Springer London |g 27/2(2015-03-01), 335-374 |x 0934-5043 |q 27:2<335 |1 2015 |2 27 |o 165 | ||