Loading presentation...

Present Remotely

Send the link below via email or IM

Copy

Present to your audience

Start remote presentation

  • Invited audience members will follow you as you navigate and present
  • People invited to a presentation do not need a Prezi account
  • This link expires 10 minutes after you close the presentation
  • A maximum of 30 users can follow your presentation
  • Learn more about this feature in our knowledge base article

Do you really want to delete this prezi?

Neither you, nor the coeditors you shared it with will be able to recover it again.

DeleteCancel

Make your likes visible on Facebook?

Connect your Facebook account to Prezi and let your likes appear on your timeline.
You can change this under Settings & Account at any time.

No, thanks

A B Formális Módszer

A B Formális Módszer
by

Zoltán Istenes

on 16 November 2011

Comments (0)

Please log in to add your comment.

Report abuse

Transcript of A B Formális Módszer

Az előadás kivonata:
A formális módszerek matematikai alapokon nyugvó eszközök szoftver és hardver rendszerek specifikációjára és fejlesztésére. A formális módszerek használata különösen terjedésnek indult, a különböző biztonságkritikus és a bizonyíthatóan helyesen működő rendszerek iránti igény növekedése miatt, mivel ezen eszközök használatával a rendszerek megbízhatóságát, robusztusságát és biztonságosságát lehet matematikai eszközökkel ellenőrizni és bizonyítani.
A B módszer egy szigorú értelembe vett formális módszer, amely szoftverkomponensek specifikációjára, tervezésére és megvalósítására szolgál, használatával lehetséges feladatokat absztrakt gépekként specifikálni, finomítani, implementálni majd futtatható kódot generálni és a rendszer helyességét bizonyítani.
A B módszer használatát, fejlesztő és helyességbizonyító környezet segíti. A B módszert több biztonságkritikus ipari alkalmazásban is felhasználták. Ismertebb alkalmazásai: a párizsi 14-es vezető nélküli metrója, a Paris-Roissy repülőtér automatikus járművei, valamint a chipkártyák.
A B formális módszer
Istenes Zoltán
istenes@inf.elte.hu

Eötvös Loránd Tudományegyetem
Informatikai Kar
Programozáselmélet és Szoftvertechnológiai Tanszék

NJSZT Szoftvertechnológiai Fórum
Budapest, 2010/06/11
B módszer - eszközök
B módszer alkalmazások
B módszer
az ELTE-IK-n
B módszer áttekintés
B nyelv
helyettesítések
bizonyítások
szintaktika
szemantika
architektúra
Atelier-B
Rodin
absztrakt gép
metró
chipkártya
autó
"Formális módszerek a szoftvertechnológiában" tárgy
FORMED 2008
TFM-B
2004: a B módszer "felfedezése" (Fóthi Ákos)
tanszéki szeminárium
választható, egy féléves kurzus
2006: meghívott előadó: Christian Attiogbe szeminárium
hallgatóknak és oktatóknak
2008: FORMED szervezés, ETAPS workshop Budapesten
Formal Methods in Computer Science Education
meghívott előadó: Jean-Raymond Abrial
2008-2010: részvétel: TFM-B konferencia
2009: "Formális Módszerek a Szoftvertechnológiában" kurzus
hallgatói szakdolgozatok,
részvétel a kutatásban
B módszer és Robotika...
B módszer + CPPCC
Certified Proved Property Carrying Code
"klasszikus-B"
"B-esemény"
B "program" példa
Irodalom
Formális módszer
B módszer (B method)
Egy formális szoftver fejlesztési módszer,
melynek segítségével egy program viselkedését lehet absztrakt módon modellezni a B nyelvben,
majd egymást követő finomításokkal, egy konkrét modellt lehet kapni, (C++ vagy ADA-ba átkódolható nyelv részhalmazt).
Egy formális bizonyítás tevékenységgel ellenőrizni lehet az absztrakt modell koherenciáját,
és minden finomítás megfelelőségét a felsőbb modellnek, így biztosítva a teljes konkrét megvalósítás megfelelését az absztrakt modellnek.
biztonság kritikus rendszerek készítésére
formális eszköz (formális szintaktika és szemantika)
B nyelv használata a specifikációtól az implementációig
helyesség bizonyítás a specifikációtól az implementációig
lépésenkénti finomítás, komponensek
automatikus kódgenerálás (C++, Java, ADA)
támogató eszközök léteznek (keretrendszerek, helyesség bizonyítók)
ipari alkalmazások léteznek
J-R Abrial,
The B-Book - Assigning Programs to Meanings,
Cambridge University Press, ISBN 0-521-49619-5


J. Wordsworth,
Software Engineering with B,
Addison Wesley Longman, ISBN 0-201-40356-0


Jean-Raymond Abrial,
Modeling in Event-B - System and Software Engineering,
Swiss Federal University (ETH), Zürich, ISBN-13: 9780521895569
szükséglet a "nagy" és "biztonságos" rendszerek iránt: biztonság kritikus rendszerek
(szigorú értelemben):
"a rendszer leírásának a szemantikája és a szintaktikája formális matematikai eszközökkel van definiálva ... és bizonyító rendszer is van hozzá..."
formális módszerek a:
specifikációban
fejlesztésben
ellenőrzésben
A B, egy eszközökkel támogatott, "absztrakt gép" jelölésrendszert használó, formális módszer, amelyt a szoftver fejlesztésben használnak...
classical B
B-event
Atelier-B
Rodin
http://www.bmethod.com
http://www.event-b.org
http://www.deploy-project.eu
http://www.clearsy.com
Jean-Raymond Abrial
követelmény specifikáció
Jean-Raymond Abrial '80
Z jelölésrendszer
halmaz elmélet
absztrakt gép fogalma

B projekt:
típus ellenőrzés
bizonyítandó állítások generálása (proof obligation generation)
bizonyítás (automatikus/interaktív)
B0 ellenőrzés
forrás kód generálás
fordítás, futtatás
autó ipar :
diagnózis (Peugeot)
érintés nélküli kártya (Renault)
bank:
egyeztetés (Societé Générale)
űrhajózás:
Ariane 5 repülési rendszer (EADS)
mikroelektronika:
chipkártyák (STMicroelectronics)
atomenergia:
vezérlő rendszer tervezés (EDF)
ipar:
pneumatikus prés (CNAM)
Thierry Lecomte (ClearSy) anyagai felhasználásával
szoftver
rendszer ("system")
műveletek (operations)
események (events)
vendégoktatók (2010-2011?):
Jean-Raymond Abrial ("B") - előadás sorozat
Thierry Lecomte (ClearSy) - ipari workshop
Christian Attiogbe (Univ. Nantes)
Dominique Méry (Univ Nancy)
The event-B Modelling Method: Concepts and Case Studies

Logics of Specification Languages
Series: Monographs in Theoretical Computer Science.
An EATCS Series
Bjorner, Dines; Henson, Martin C. (Eds.)
ISBN: 978-3-540-74106-0
cél: rendszer szintű bizonyítás szoftver specifikáció számára
"a szoftver szint nem (mindig) elég..."
METEOR (metró 14-es vonal, Párizs)
vezető nélküli...
1998-tól...
117.000 B sor
29.000 tétel
87.000 ADA sor
v1.0 (2010) !
Párizsi CDG repülő téri automatikus metró
180.000 B sor
43.000 tétel
140.000 ADA sor
98% automatikusan bizonyítva
Platform Screen Doors (PSD)
a PSD-nek 9.999/10.000 ki kell nyílnia,
ha "érvényes" vonat álló helyzetben van,
és kinyitja az ajtaját...

project: 4 hónap, 3 állomás
csapat: 1 projekt menedzser, 1 fejlesztő, 1 "validation engineer", 1 biztonsági mérnök
rendszer szintű, funkcionális leírás: 130 oldal
biztonsági esetek: 300 oldal
fejlesztési dokumentáció: 600 oldal (30 dok.)
B model: 3.500 sor, 1.000 bizonyítandó állítás,
90% automatikusan bizonyítva, interaktív bizonyítás 2 nap alatt...
kísérlet: 8 hónap, 96.000 vonat, 0 hiba
B, for the design of proven systems and software

B is a formal specification method which, thanks to an adequate language, allows for highly accurate expressions of the properties required by specifications. One can then prove in a fully automated fashion that these properties are unambiguous, coherent and are not contradictory. This then allows us to mathematically prove that these properties are taken into account as the design stages progress.

Therefore, this method and its associated proof allow for:

Clear technical specifications and system specifications to be reached that are structured, coherent and unambiguous,
The development of software that is contractually guaranteed to be fault-free, in areas such as real time, industrial automatisms, communication protocols, cryptographic protocols, onboard IT…
The B Method

B Method usually refers to the set that includes: B language, refinement, proof and related tools.

B development starts with the writing of a concrete model that includes all of the defined needs. The main data processed by the system is described, as well as the fundamental properties of this data. Services ensure the processing of this data while preserving its properties. The B model thus obtained is a specification of what the system should create.

The B model is then transformed (refined with B vocabulary) until a complete software installation of the software is obtained.

Finally, we arrive at a concrete model, proven and fault-free, that can be coded into C or Ada language.

B Method is therefore: "a proven construction approach (referred to as correct) based on B Language, refinement and proof."
"Event-B, to analyze, study and specify, not only software, but also whole systems..."
ProB - animátor, modell ellenörző
Brama - animátor
Bart - automatikus finomító
CompoSys - rendszer architektúra tervező
RODIN2B
B2RODIN
B4SYN - VHDL fordító
B2LADDER - LADDER fordító
ComenC - C fordító
B műveletek definiálása helyettesítésekkel
adat transzformáció
nem determinisztikus...
általánosított helyettesítés
(generalized substitution)
kapcsolódási (láthatósági) szabályok...
cél: a komplexitás csökkentése
REFINES, IMPORTS, SEES, INCLUDES, PROMOTES, EXTENDS, USES
formális módszerek szükségesek ezen rendszerek "megbízhatóságának" a bizonyítására
"architektúra" (gépek kapcsolódása)
helyettesítés
(substitution)
bizonyítás
megfelel a megrendelő elvárásainak
vs.
megfelel a specifikációnak
COQ (formális bizonyítás kezelő rendszer)
a B-módszer bizonyítása...
classical B
B-event
formális módszer
bizonyítás
követelmény specifikációk
finomítás
Val de Roissy Shuttle automatikus vonat:
automatikus finomítás
kb. 700 finomító szabály, kb. fele fejlesztési idő
EU FP7
"What You Get Is What You Provided..."
ELTE-IK-PSZT
MSc
Szoftver technológiai modul
2 féléves kurzus
előadás és gyakorlat
Formális Módszerek a Szoftvertechnológiában
technológiai megközelítés
"teljes" szoftvertechnológiai folyamat... kódgenerálás...
hallgatók erős matematikai alapokkal
hallgatók formális és módszertani ismereteire támaszkodik
új fogalmak bevezetése sok példával
sok házifeladat
"nemzetközi kapcsolatok"
vasút
/* csg
* Author:
* Creation date: P márc. 12 2010
*/
MACHINE
csg
CONSTANTS
maxkassza10,
maxkassza20,
maxkiscsoki,
maxnagycsoki
PROPERTIES
maxkassza10 : NAT & maxkassza10 = 10
& maxkassza20 : NAT & maxkassza20 = 5
& maxkiscsoki : NAT & maxkiscsoki = 5
& maxnagycsoki : NAT & maxnagycsoki = 5
VARIABLES
kiscsoki,
nagycsoki,
kassza10,
kassza20,
bedobott
INVARIANT
kassza10 : NAT & kassza10 <= maxkassza10
& kassza20 : NAT & kassza20 <= maxkassza20
& kiscsoki : NAT & kiscsoki <= maxkiscsoki
& nagycsoki : NAT & nagycsoki <= maxnagycsoki
& bedobott : NAT
& bedobott <= kassza10*10+kassza20*20-10*maxkiscsoki
& (maxkiscsoki-kiscsoki)*10 + (maxnagycsoki-nagycsoki)*20 +maxkiscsoki*10
=
(kassza10*10) + (kassza20*20) - bedobott



INITIALISATION
kiscsoki := maxkiscsoki
|| nagycsoki := maxnagycsoki
|| kassza10 := maxkiscsoki
|| kassza20 := 0
|| bedobott := 0
OPERATIONS
szerviz =
PRE
bedobott = 0
THEN
kiscsoki := maxkiscsoki
|| nagycsoki := maxnagycsoki
|| kassza10 := maxkiscsoki
|| kassza20 := 0
END
;
bedob10 =
PRE
kassza10 < maxkassza10
THEN
bedobott := bedobott + 10 ||
kassza10 := kassza10 + 1
END
;
kerkiscsoki =
PRE
bedobott >= 10 & kiscsoki > 0
THEN
bedobott := bedobott - 10
|| kiscsoki := kiscsoki - 1
END
;
kernagycsoki =
PRE
bedobott >= 20 & nagycsoki > 0
THEN
bedobott := bedobott - 20
|| nagycsoki := nagycsoki - 1
END
;
bedob20 =
PRE
kassza20 < maxkassza20
THEN
bedobott := bedobott + 20 ||
kassza20 := kassza20 + 1
END
;

visszaad =
ANY
vissza10,vissza20
WHERE
vissza10:0..kassza10
& vissza20:0..kassza20
& (vissza10*10) + (vissza20*20) = bedobott
THEN
bedobott := 0
|| kassza10 := kassza10 - vissza10
|| kassza20 := kassza20 - vissza20
END



END
/* csg_i
* Author:
* Creation date: P márc. 12 2010
*/
IMPLEMENTATION
csg_i
REFINES
csg
VALUES
maxkassza10 = 10;
maxkassza20 = 5;
maxkiscsoki = 5;
maxnagycsoki = 5


CONCRETE_VARIABLES
kiscsoki,
nagycsoki,
kassza10,
kassza20,
be10, be20

INVARIANT
kassza10 : NAT & kassza10 <= maxkassza10
& kassza20 : NAT & kassza20 <= maxkassza20
& kiscsoki : NAT & kiscsoki <= maxkiscsoki
& nagycsoki : NAT & nagycsoki <= maxnagycsoki
& be10 : NAT & be20 : NAT
& be10<=kassza10-kiscsoki & be20<=kassza20
& bedobott = 10*be10 + 20*be20
& (maxkiscsoki-kiscsoki)*10 + (maxnagycsoki-nagycsoki)*20 +maxkiscsoki*10
=
(kassza10*10) + (kassza20*20) - bedobott




INITIALISATION
kiscsoki := maxkiscsoki;
nagycsoki := maxnagycsoki;
kassza10 := maxkiscsoki;
kassza20 := 0;
be10 := 0; be20 := 0


OPERATIONS
szerviz =
BEGIN
kiscsoki := maxkiscsoki;
nagycsoki := maxnagycsoki;
kassza10 := maxkiscsoki;
kassza20 := 0
END
;
bedob10 =
BEGIN
be10 := be10 + 1;
kassza10 := kassza10 + 1
END
;
kerkiscsoki =
BEGIN
IF be10 = 0 THEN
be10 := 1;
be20 := be20 -1;
kiscsoki := kiscsoki - 1
ELSE
be10 := be10 - 1;
kiscsoki := kiscsoki - 1
END

END
;
kernagycsoki =
BEGIN
IF be20 = 0 THEN
be10 := be10-2
ELSE
be20 := be20 - 1
END;
nagycsoki := nagycsoki - 1
END
;
bedob20 =
BEGIN
be20 := be20 + 1;
kassza20 := kassza20 + 1
END



;
visszaad =
BEGIN

kassza10 := kassza10 - be10;
kassza20 := kassza20 - be20;
be10 := 0; be20 := 0
END


END
THEORY User_Pass IS
Operation(szerviz) & ff(0) & pp;
Operation(szerviz) & ff(0) & pr & pp;
Operation(bedob10) & ff(0) & ss & pp(rp.1);
Operation(kerkiscsoki) & ff(0) & pp;
Operation(kerkiscsoki) & ff(0) & ss & pp(rp.1);
Operation(kernagycsoki) & ff(0) & pp;
Operation(kernagycsoki) & ff(0) & ss & pp(rp.1);
Operation(bedob20) & ff(0) & ss & pp(rp.1);
Operation(visszaad) & ff(0) & ss & pp;
Operation(visszaad) & ff(0) & ss & pp(rp.1)
END
képzési eredmények:
a hallgatók még több tudást gyűjtenek szoftvertechnológiai és formális módszerekkel kapcsolatos fogalmakkal és technikákkal kapcsolatban
képessé válnak követelményeket specifikálni, programokat tervezni és bizonyítani (olyan programokat "teljesen" bizonyított programokat készíteni amelyek "megfelelnek" a specifikáiójuknak
A projekt az Európai Unió támogatásával,
az Európai Szociális Alap társfinanszírozásával valósul meg
(a támogatás száma TÁMOP 4.2.1./B-09/1/KMR-2010-0003).
3. óra
Building Access Control
specif & interakció
Predicates Transformations invariants
"Gyenge az invariáns!!!"
villamos
sebességváltó
specif ellenőrzés B-vel
specif elméleti "működés" - ProB-vel
Full transcript