Français Anglais
Accueil Annuaire Plan du site
Accueil > News du laboratoire > Séminaire Digiteo, Jim Woodcock, The token experiment
Séminaire Digiteo, Jim Woodcock, The token experiment
Séminaire Digiteo, Jim Woodcock, The token experiment Séminaire Digiteo, Jim Woodcock, The token experiment
19 mai 2009

PUIO, 19 Mai, 10h30

The Tokeneer project is one of the most important contributions to the Verified Software Repository (VSR): it has been described by Tony Hoare as "a milestone in the transfer of program verification technology into industrial applic
Jim Woodcock is Professor of Software Engineering at the University of York.  His current research interests are in program verification and model checking, particularly applied to industrial-scale systems.  He is verifying the correctness of a large xUML model of railway European signalling, a flash-based filestore for critical embedded applications, and a real-time operating system.  He is the moderator for the UK Grand Challenge in Dependable Systems Evolution.

A Token Experiment

The Tokeneer project is one of the most important contributions to the Verified Software Repository (VSR): it has been described by Tony Hoare as "a milestone in the transfer of program verification technology into industrial application".  The project was a demonstration of the feasibility of cost-effective development of highly secure systems to the level of rigour required by the upper assurance levels of the Common Criteria.  It was carried out by Praxis for the US National Security Agency, and involved the re-development of part of the existing Tokeneer secure system following the Praxis correct-by-construction process.  Only two bugs have been found since the system went live in 2003.  A version of the entire project archive has been released as part of the VSR.  

Is there anything else we can say about Tokeneer?  Can we break it?  We report on the results of an experiment using model-based testing to explore the system's dependability.  Our technique has discovered 12 "interesting" scenarios that can be played out using the Tokeneer simulator (part of the released archive).  We will present as many of these as time allows. 

News
George Manoussakis, lauréat 2018, prix de thèse (accessit) Charles Delorme
18 septembre 2018
George Manoussakis, est lauréat de prix de thèse (accessit) Ch. Delorme 2018. Il a soutenu sa thèse au LRI/Galac en Novembre 2017 sous la direction de J. Cohen et A. Deza. Depuis Septembre 2018 il est MdeC à l'Université de Versailles/Li-PaRAD.

TrackML dans Nature
21 janvier 2018
L'apprentissage automatique peut-il aider la physique des hautes énergies à découvrir et à caractériser de nouvelles particules ? TAO participe à l'organisation du challenge TrackML avec le CERN. La seconde phase de la compétition utilisera Codalab.

Un article de Isabelle Guyon sur la démocratisation de l'IA
19 mars 2018
Lien vers l'article paru dans le journal le monde :
http://www.lemonde.fr/acces-restreint/sciences/article/2018/04/08/a4544bd07cad09fe52980c0f82c08b34_5282548_1650684.html