Email Gateway (Aug 18 2022 at 19:19): Email Gateway (Aug 18 2022 at 19:19):From: Burkhart Wolff <Burkhart.Wolff@lri.fr>
Dear all,
here are 3 new papers concerning "Isabelle and Testing/Refinement":
[1] Achim D. Brucker, Burkhart Wolff: On Theorem Prover-based Testing. Accepted the 07-08-2011. In Formal Aspects of Computing (FAOC). DOI: 10.1007/s00165-012-0222-y. Springer, 2012.
Abstract:
HOL-TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. As such, HOL-TestGen allows for an integrated workflow supporting
interactive theorem proving, test case generation, and test data generation. The HOL-TestGen method is two-staged: first, the original formula is partitioned into test cases by transformation into
a normal form called test theorem. Second, the test cases are analyzed for ground instances (the test data) satisfying the constraints of the test cases. Particular emphasis is put on the control
of explicit test-hypotheses which can be proven over concrete programs. Due to the generality of the underlying framework, our system can be used for black-box unit, sequence, reactive sequence
and white-box test scenarios. Although based on particularly clean theoretical foundations, the system can be applied for substantial case-studies (see [2]).
This reference supersedes all older papers concerning HOL-TestGen.
(Like the original Fates Paper or the TAP 2007 paper).
Link: http://www.lri.fr/~wolff/papers/journals/brucker.ea-hol-testgen-2008.rev-1.pdf
[2] Achim D. Brucker, Lukas Brügger, Paul Kearney, and Burkhart Wolff. An approach to modular and testable security models of real-world health-care applications.
Proceedings of the ACM Symposium on Access control models and technologies, pages 133-142. ACM, 2011. SACMAT 2011. [ bib ]
Abstract:
We present a generic modular policy modelling framework and instantiate it with a substantial case study for model- based testing of some key security mechanisms of applica- tions and services of the NPfIT.
NPfIT, the National Pro- gramme for IT, is a very large-scale development project aiming to modernise the IT infrastructure of the National Health Service (NHS) in England. Consisting of heterogeneous and distributed
applications, it is an ideal target for model-based testing techniques of a large system exhibiting critical security features.
We model the four information governance principles, com- prising a role-based access control model, as well as policy rules governing the concepts of patient consent, sealed envelopes and legitimate relationships.
The model is given in Higher-order Logic (HOL) and processed together with suitable test specifications in the HOL-TestGen system, that generates test sequences according to them. Particular em- phasis is put on the
modular description of security policies and their generic combination and its consequences for model-based testing.
Link: http://www.brucker.ch/bibliography/download/2011/brucker.ea-model-based-2011.pdf
[3] Abderrahmane Feliachi, Marie-Claude Gaudel, and Burkhart Wolff. Isabelle/circus: A process specification and verification environment.
In VSTTE, volume 7152 of Lecture Notes in Computer Science, pages 243-260, 2012. [ bib ]
Abstract: TheCircus specification language combines elements for complex data and behavior specifications, using an integration of Z and CSP with a refinement calculus. Its semantics
is based on Hoare and He’s unifying theories of programming (UTP). We develop a machine-checked, formal semantics based on a “shallow embedding” of Circus in Isabelle/UTP
(our semantic theory of UTP based on Isabelle/HOL). We derive proof rules from this semantics and implement tactic support that finally allows for proofs of refinement for Circus processes
(involving both data and behavioral aspects). This proof environment supports a syntax for the semantic definitions which is close to textbook presentations of Circus.
Link: http://www.lri.fr/~wolff/papers/conf/VSTTE-IsabelleCircus11.pdf
Enjoy !
bu
Email Gateway (Aug 18 2022 at 19:19):From: Thomas Genet <thomas.genet@irisa.fr>
Dear all,
Email Gateway (Aug 18 2022 at 19:19):From: Burkhart Wolff <Burkhart.Wolff@lri.fr>
Am 15.03.2012 um 13:39 schrieb Thomas Genet:
Dear all,
Le 14/03/12 18:39, Burkhart Wolff a écrit :
Dear all,
here are 3 new papers concerning "Isabelle and Testing/Refinement":
maybe this is naive question, but how do HOL-testgen behaves w.r.t. quickcheck and nitpick tools of Isabelle/HOL?
HOL-TestGen follows a completely independent symbolic approach to test-case generation (via normalization)
and test data selection. It has nothing to do with nitpick (essentially: counter-example generation for finitized
interpretations of a formula), but uses potentially quickcheck and smt (i.e. Z3) in the test data selection phase.
Is it likely to succeed to find a counterexample where a typical
quickcheck [tester=narrowing]
call fails?
That depends from the application domain.
I can not make any statistical guessing here.
For the problems we are mostly using it -
model-based testing in security related domains -
there is no hope that the finitized interpretation method
does any good, though.
bu
Last updated: Apr 25 2024 at 01:08 UTC