[isabelle] papers available

Dear all,

it is a pleasure to present two papers for the research field "Test&Proof", 
aiming at novel combinations of (Isabelle)-proofs and test-generation techniques.

A) Authors: A. Brucker, L. Brügger, P. Kearney and Burkhart Wolff:
  Title: Verified Firewall Policy Transformations for Test Case Generation
      We present an optimization technique for model-based generation of test cases 
   for firewalls. Based on a formal model for firewall policies in higher-order logic, 
   we derive a collection of semantics-preserving policy transformation rules and an 
   algorithm that optimizes the specification with respect of the number of test 
   cases required for path coverage.  The correctness of the rules and the algorithm 
   is established by formal proofs in Isabelle/HOL. Finally, we use the normalized 
   policies to  generate test cases with the domain-specific firewall testing tool 
    The resulting procedure is characterized by a gain in efficiency
    of two orders of magnitude and can handle configurations with
    hundreds of rules as occur in practice.
   Appeared in ICST 2010, URL: .pdf
B) Authors: A. Brucker, L. Brügger, P. Kearney, and B. Wolff. 
      Title: An approach to modular and testable security models of real-world health-care applications.
      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 heteroge- neous 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 en- velopes and legitimate relationships. The model is given in 
       Higher-order Logic (HOL) and processed together with suit- able 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.

      To appear in SACMATR 2011, URL: http://www.lri.fr/~wolff/papers/conf/2011-sacmat-mbtsec-npfit.pdf

Enjoy !


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.