Monday, January 2, 2017

11th International Conference on Tests And Proofs TAP 2017

First Call for Papers

11th International Conference on Tests And Proofs
TAP 2017 Marburg (Germany), 19-20 July 2017

Part of STAF 2017

Important Dates

Abstract:             17 February 2017
Paper:                24 February 2017
Notification:          7 April 2017
Camera-Ready Version: 21 April 2017
Conference:           17-21 July 2017

Aim and Scope

The TAP conference promotes research in verification and formal
methods that targets the interplay of proofs and testing: the
advancement of techniques of each kind and their combination, with the
ultimate goal of improving software and system dependability.

Research in verification has recently seen a steady convergence of
heterogeneous techniques and a synergy between the traditionally
distinct areas of testing (and dynamic analysis) and of proving (and
static analysis). Formal techniques, such as model checking, that
produce counterexamples when verification fails are a clear example of
the duality of testing and proving. The combination of static
techniques such as satisfiability modulo theory and predicate
abstraction has provided means of proving correctness by complementing
exhaustive enumeration testing-like techniques. More practically,
testing supports the cost-effective debugging of complex models and
formal specifications, and is applicable in conditions that are beyond
the reach of formal techniques -- for example, components whose source
code is not accessible. Testing and proving are increasingly seen as
complementary rather than mutually exclusive techniques.

The TAP conference aims to promote research in the intersection of
testing and proving by bringing together researchers and practitioners
from both areas of verification.

Topics of Interest

TAP's scope encompasses many aspects of verification technology,
including foundational work, tool development, and empirical
research. Its topics of interest center around the connection between
proofs (and other static techniques) and testing (and other dynamic
techniques). Papers are solicited on, but not limited to, the
following topics:

- Verification and analysis techniques combining proofs and tests
- Program proving with the aid of testing techniques
- Deductive techniques (theorem proving, model checking, symbolic
execution, SMT solving, constraint logic programming, etc.) to
support testing: generating testing inputs and oracles, supporting
coverage criteria, and so on.
- Program analysis techniques combining static and dynamic analysis
- Specification inference by deductive and dynamic methods
- Testing and runtime analysis of formal specifications
- Model-based testing and verification
- Using model checking to generate test cases
- Testing of verification tools and environments
- Applications of testing and proving to new domains, such as
security, configuration management, and language-based techniques
- Bridging the gap between concrete and symbolic reasoning techniques
- Innovative approaches to verification such as crowdsourcing and
serious games
- Case studies, tool and framework descriptions, and experience
reports about combining tests and proofs

Highlight Topics

In addition to TAP’s general topics of interests, the 11th edition of
TAP will feature two highlight topics on techniques, tools, and
experience reports on

1. Testing and proving the correctness of security properties and
 implementations of cryptographic functions and protocols with a
 focus on the successful interplay of tests and proofs, and

2. Asserting the correct functioning and testing of verification
 tools, especially on theorem provers, that form the basis of many
 verification results for tools and applications our society
 increasingly depends on.

Submission Instructions

TAP 2017 accepts papers of three kinds:

- Regular research papers: full submissions describing original
research, of up to 16 pages (excluding references).

- Tool demonstration papers: submissions describing the design and
implementation of an analysis/verification tool or framework, of up
to 8 pages (excluding references). The tool/framework described in
a tool demonstration paper should be available for public use.

- Short papers: submissions describing preliminary findings, proofs
of concepts, and exploratory studies, of up to 6 pages (excluding


Program Chairs

- Einar Broch Johnsen
- Sebastian Gabmeyer

Program Committee

- Bernhard K. Aichernig
- Elvira Albert
- Bruno Blanchette
- Jasmin C. Blanchette
- Achim D. Brucker
- Catherine Dubois
- Gordon Fraser
- Carlo A. Furia
- Sebastian Gabmeyer (chair)
- Angelo Gargantini
- Alain Giorgetti
- Christoph Gladisch
- Martin Gogolla
- Arnaud Gotlieb
- Marieke Huisman
- Bart Jacobs
- Einar Broch Johnsen (chair)
- Nikolai Kosmatov
- Laura Kovacs
- Martin Leuker
- Panagiotis Manolios
- Karl Meinke
- Andreas Podelski
- Andrew J. Reynolds
- Martina Seidl
- Martin Steffen
- Martin Strecker
- T. H. Tse
- Luca Viganò
- Burkhart Wolff
- Stijn de Gouw

events mailing list

ABZ 2018

5-8 June 2018, Southampton, U.K.

Saturday, June 4, 2016

An Incremental B-Model for RBAC-Controlled Electronic Marking System

Nasser Al-hadhrami (Ministry of Education, Nizwa, Oman), Benjamin Aziz (School of Computing, University of Portsmouth, Portsmouth, UK) and Lotfi ben Othmane (Fraunhofer Institute for Secure Information Technology, Darmstadt, Germany)

Modelling and Refining Hybrid Systems in Event-B and Rodin

Sunday, March 27, 2016

Principle of Beneficent Difficulty, M. Jackson

 "Principle of Beneficent Difficulty

 Difficulties, explicitly characterized and diagnosed, are the medium in which a method captures its central insights into a problem. A method without limitations, whose development steps are never impossible to complete, whose stages diagnose and recognise no difficulty, must be very bad indeed. Just think about it. A method without limitations and difficulties is saying one of two things to you. Either it’s saying that all problems are easily solved. You know that’s not true. Or else it’s saying that some problems are difficult, but the method is not going to help you to recognise or overcome the difficult bits when you meet them. Take your choice. Either way it’s bad news. "

Michael Jackson. Software Requirements and Specifications: A Lexicon of Principles, Practices and Prejudices. Addison-Wesley and ACM Press, 1996


L'exemple classique (fourni par Mike Spivey dans La notation Z, Masson, traduit par Michel Lemoine, 1994) 
Le carnet d'anniversaire 
Nous utilisons, quand c'est possible, la notation ASCII de B. 

NOM et DATE sont des types de base (les SETS de B) 
Voici de qu'en Z, on appelle des schémas : 
    connu : POW (NOM)
    anniversaire : NOM +-> DATE
    connu = dom (naissance)
    nom? : NOM
    date? : DATE
     nom? /: connu
    anniversaire' = anniversaire \/ {nom? |-> date?}

DELTA déclare : connu, connu', anniversaire, anniversaire'. Le prime exprime l'état après l'opération. 
Attention ! 
Vous avez bien lu. Ci-dessus, nous avons écrit = et non :=. Un schéma est un prédicat. Le saut de ligne exprime une conjection. 
Le schéma AjoutAnniversaire donne le prédicat qui doit être respecté par l'opération d'ajout. 
    nom? : NOM
    date! : DATE
    nom? : connu
    date! : anniversaire (nom?)
  KHI déclare : connu, connu', anniversaire, anniversaire' et les contraintes : 
connu = connu' 
anniversaire' = anniversaire 
Un schéma va permettre de spécifier un état initial, lequel, comme en B, sert à s'assurer que l'on peut bien avoir un état satisfaisant les contraintes. 
    connu = { }
________________________________________ RAPPORT ::= ok | déjàConnu | nonConnu

RAPPORT est un type libre. 
    résultat! : RAPPORT
    résultat! = ok
    nom? : NOM
    résultat! : RAPPORT
    nom? : connu
    résultat! = déjàConnu

Utilisation du schéma calculus : 
On va avoir une spécification robuste 
RAjoutAnniversaire == (AjoutAnniversaire & Succès) or DéjàConnu
Il y a d'autres opérateurs que le & et le or pour le calcul de schémas. 
Nous avons présenté des schémas fermés. Les déclarations sont locales à ces schémas. 
Il existe des schémas ouverts (description axiomatique) qui introduisent une ou plusieurs variables globales et éventuellement spécifient une contraintes sur leurs valeurs. 
Exemple : 
    carré : NAT --> NAT
    ! b: NAT . carré(n) = n * n

La notation Z pour la description des ensembles en compréhension : 
{...| ... ....} 
On distingue trois parties {déclaration | contrainte . expression } 
exemple : 
{x : NAT | pair (x) . x * x} est l'ensemble des carrés des nombres pairs.
Les schémas comme types 
On peut prendre un schéma comme type. 
Un schéma est alors vu comme l'ensemble des états qui respectent le schéma. Une variable de type schéma est alors une variable qui peut prendre comme valeur un de ces états qui respectent le schéma indiqué comme type de la variable. 
=======[X, Y] =============================
    first : X * Y --> X
    !x : X ; y : Y . first(x, y) = x

En français, deux livres sur Z. 
Une introduction avec 
D. Lightfoot, Spécification formelle avec Z, Teknea, traduit par H. Habrias 
J.M. Spivey, La notation Z, Masson, traduit par M. Lemoine

B événementiel, l'île et le pont de J.R. Abrial

Source : Présentation de J.R. Abrial (Janvier 2000) 
Le contrôleur du pont de l'île 
Le principe : le saut en parachute. 

Plus on s'approche du sol, plus on voit de choses, plus on voit d'événements.
Première vue du système (ou modèle initial) 
Quelles sont les données ? 
On a une seule variable, n, le nombre de véhicules qui sont dans le système. 
De plus, le nombre maximum de véhicules que peut contenir le système est constant (d) 
La contrainte à satisfaire est : 
0 <= n <= d
La forme générale d'un événement pour cette présentation 
       < garde>
    < action>

On a deux événements 
Sortie du continent vers le système 
        n < d
        n := n+ 1

Entrée sur le continent 
ML_IN ==
        n > 0
        n := n - 1

Les obligations de preuve 
1) La préservation de l'invariant 
Etant donné un événement de forme générale : EVENT ==
        x := E(x)
et un invariant I(x) à préserver, il faut prouver que :
I(x) & G(x) => I(E(x))

Soit dans notre cas 
pour l'événement ML_OUT 
0 <= n <= d & n 0 <= n + 1 <= d 
pour l'événement ML-IN 
0 <= n <= d & n 0 <= n - 1 <= d 
2) Preuve de vivacité (liveness) 
 Etant donné un système d'événements avec les gardes :
G1 (x), ..., Gn (x) et un invariant I(x), l'énoncé à prouver est :
I(x) => G1(x) or ...or Gn(x)
i.e. un événement au moins est toujours prêt à être déclenché (ABSENCE DE VERROU FATAL)

Soit ici : 
0 <= n <= d => 0 < n or n < d 
Ce que l'on ne peut prouver ! 
Quand n = 0, on ne peut prouver n < d 
On a oublié 0 < d 
Il y a un deadlock si d = O (plus aucune voiture ne peut entrer). 
On corrige donc et alors on peut prouver que : 
0 <= n <= d  & 0 < d => 0 < n or n < d 
3) Preuve d'absence de sous-boucles infinies 
Pour chaque événement (dans le cas de deux événements seulement) : 
    WHEN G(x) THEN x := E(x) END Il faut prouver, étant donné un invariant I(x) :
I(x) => 0 <= V(x) &
I(x) & G(x) =< V (E(x)) < V(x)
où V(x) est un variant à exhiber pour chaque événement.

Soit ici 
Pour ML_OUT, un variant est d - n 
0 <= n <= d & 0 < d => 0 <= d - n 
0 <= n <= d & 0 < d & n < d 
d - (n + 1) < d - n 
Pour ML_IN, un variant est n 
0 <= n <= d & 0 < d => 0 <= n 
0 <= n <= d & 0 < d & n < d 
n -1 <  n 
Deuxième vue du système , raffinage par introduction du pont 
On est descendu  et on aperçoit maintenant le pont. 
On voit : 
- des véhicules sur le pont qui se dirigent vers l'île (un nombre n)
- des véhicules qui sont dans l'île (un nombre b)
- des véhicules qui se dirigent vers le contenant (un nombre c)
0 <= a &
0 <= b &
0 <= c &
a = 0 or c = 0 /* tous les véhicules vont dans la même direction */

Invariant de collage 
a + b + c = n

Les techniques de raffinage : 
1) Chaque événement est raffiné par un événement concret 2) Le monde abstrait travaille avec x et le concret avec y
3) Un invariant de collage I(x, y) lie les deux mondes

Les mécanismes de raffinage sont : 
- le renforcement des gardes (normal, plus on voit de choses en s'approchant du sol, plus on voit de contraintes. C'est bien connu, quand on est "haut placé" on est en dehors des contingences matérielles...voilà sans doute pourquoi certains recherchent ces places...dans les amphis (?!))     Rappel : en ce qui concerne les préconditions, on les affaiblit lors du raffinage.
- des actions "simultanées" sur l'invariant de collage.

Dans notre cas, 
1) Raffinage de l'événement abstrait 
ML_OUT == WHEN n < d THEN n := n + 1 END 
en : 
ML_OUT == 
        a + b + c < d & c = 0  /* On a renforcé la garde */ 
        a := a + 1 
Raffinage de l'autre événement abstrait : 
ML_IN == 
        n > 0 
        n := n + 1 
en : 
ML_IN == 
            c > 0 
            c := c - 1 
2) Spécification des nouveaux événements 
IL_IN == 
        a > 0 
        a, b := a - 1, b + 1 
IL_OUT == 
        b > 0 & 
        a = 0 
        b, c := b - c, c + 1 
Les obligations de preuve du raffinage d'événement 
Etant donné un événement abstrait  et un événement concret correspondant EVENT == WHEN G(x) THEN x := E(x) END
EVENT == WHEN H(y) THEN y := F(y) END
et les invariant I(x) (supposé être déjà préservé par l'événement abstrait) et J(x, y),
I(x) & J(x, y) & H(y) => G(x)
I(x) & J(x, y) & H(y) => J(E(x), F(y))

à vous maintenant d'appliquer cela... 
Les niveaux suivants seront : 
1) Introduction de deux feux de circulation à chaque entrée du pont 
2) Introduction de capteurs  (il faut bien compter les véhicules pour vérifier l'invariant fourni au premier niveau) à l'entrée et à la sortie du pont 
Puis introduction du contrôleur qui : 
- décide quand les feux doivent changer
- n'a pas accès aux variables physiques
- a accès à des variables de contrôle
- qui sont des copies de variables physiques

    - qui représentent ce que le contrôleur croit de la situation physique 
    - dont les valeurs peuvent être différentes de celles des variables physiques 
            mais néanmoins le système doit fonctionner correctement comme celà est prescrit par les vairiables physiques 
- conservées en mémoire du contrôleur 
3) Introduction des canaux de communication 
        - entre le monde physique et le contrôleur (annonce de l'arrivée ou du départ d'un véhicule) 
        - entre le contrôleur et le monde physique (pour faire changer) 
Des hypothèses temporelles doivent être faites (par exemple que les capteurs physiques sont moins réactifs que les autres événements) 
4) Réunion des variables physiques et des variables canaux pour former une seule entité, l'environnement fait de : 
        - des variables physiques et des variables canaux 
        - tous les événements physiques 
        - deux services d'entrée/sortie