communications of the acm september vol no

Patrick Cousot

Description

Niveau: Supérieur, Doctorat, Bac+8
54 communications of the acm | september 2008 | vol. 51 | no. 9 practice T HE SOFT WARE ENGINEERING community has devised many techniques, tools, and approaches aimed at improving software reliability and dependability. These have had varying degrees of success, some with better results in particular domains than others, or in particular classes of applications. A popular, although not uncontroversial, approach is known as formal methods, whereby a specification notation with formal semantics, along with a deductive apparatus for reasoning, is used to specify, design, analyze, and ultimately implement a hardware or software (or hybrid) system. Such an approach is often thought to be difficult to apply and to require significant mathematical experience.1, 11 Experience has demonstrated that developers without significant mathematical ability can at least understand and use formal specifications, even if greater mathematical ability and specialization in various areas of math- ematics and engineering are needed for more challenging formal methods- related activities such as verification and refinement, and even the task of writing formal specifications them- selves. As automated formal methods slowly become a natural part of the de- sign process, we also experience higher dependability levels as a standard trait of software products. A key issue, however, is the need for those applying formal methods to be able to abstract and to model systems at an appropriate level of representation— that is, to develop solid design princi- ples and apply them to software devel- opment.

• achieved via software rather


• engineer- ing product


• concurrency can


• software engineering


• safety


• complex sys- tems


• memory safety


• safety proving


• normal design

Sujets

• London
• Software engineering
• Safety
• Memory safety

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 10
• Langue: English
• Poids de l'ouvrage: 10 Mo

Extrait

pràCTICE

D o i : 1 0 . 1 1 4 5 / 1 3 7 8 7 2 7 . 1 3 7 8 7 4 2

The answer to software reliability concerns may lie in formal methods.

BY miKe hincheY, michael JacKson, PatRicK cousot, BYRon cooK, Jonathan P. BoWen, anD tiziana maRGaRia sOFTwàrE eNgINEErINg àNd fOrMàL mETHOdS

T H ES O F T WA R EE N G I N E E R I N G cOmmUnIty Has devIsed many tecHnIqUes, tOOls, and apprOacHes aImed at ImprOvIng sOftware relIabIlIty and dependabIlIty. THese Have Had varyIng degrees Of sUccess, sOme wItH better resUlts In partIcUlar dOmaIns tHan OtHers, Or In partIcUlar classes Of applIcatIOns. A pOpUlar, altHOUgH nOt UncOntrOversIal, apprOacH Is knOwn as formal methods, wHereby a specIficatIOn nOtatIOn wItH fOrmal semantIcs, alOng wItH a dedUctIve apparatUs fOr reasOnIng, Is Used tO specIfy, desIgn, analyze, and UltImately Implement a Hardware Or sOftware (Or HybrId) system. SUcH an apprOacH Is Often tHOUgHt tO be dIfficUlt tO apply and tO reqUIre sIgnIficant matHematIcal 1, 11 experIence. ExperIenceHas demOnstrated tHat develOpers wItHOUt sIgnIficant matHematIcal abIlIty can at least Understand and Use fOrmal specIficatIOns,

54 c o m m u n i c at i o n so ft h eac m| s2 0 0 8e p t e m b e r|5 1o l . v|o. 9 n

évén if géàté àtéàticàl àbility ànd specialization invàiôus àéàs ôf àt- éàtics ànd énginééing àé néédéd fô ôé càllénging fôàl étôds- élàtéd àctivitiés suc às véificàtiôn ànd éfinéént, ànd évén té tàsk ôf witing fôàl sécificàtiôns té- sélvés. As àutôàtéd fôàl étôds slôwly bécôé à nàtuàl àt ôf té dé- sign ôcéss, wé àlsô éxéiéncé igé dééndàbility lévéls às à stàndàd tàit ôf sôftwàé ôducts. A kéy issué, ôwévé, is té nééd fô tôsé àlying fôàl étôds tô bé àblé tô àbstàct ànd tô ôdél systés àt àn àôiàté lévél ôf ééséntàtiôn— tàt is, tô dévélô sôlid désign inci- lés ànd àly té tô sôftwàé dévél- ôént. Tis is àticulàly tué wén ôving ôétiés ôf ôé côléx sys- tés invôlving significànt côncuéncy ànd intéàctiôn àông côônénts. Wén wé wis tô ôvé ôétiés, it is ôftén éàsié—ànd nécéssày—tô ôvé té àt à ôé àbstàct lévél, éxlôiting té idéà ôfabstract interpretation. Tis àticlé côntàins côntibutiôns fô téé wôld-énôwnéd éxéts in té fiélds ôf sôftwàé énginééing, àb- stàct intéétàtiôn, ànd véificàtiôn ôf côncuént systés: Micàél A. Jàck- sôn, Pàtick Côusôt, ànd Byôn Côôk. Téi côntibutiôns àé bàséd ôn téi kéynôté séécés àt té IEEE’s Fift In- ténàtiônàl Cônfééncé ôn Sôftwàé En- ginééing ànd Fôàl Métôds, éld in Lôndôn, Sét.10–14, 2007. Té ài ôf té cônfééncé séiés is tô bing tôgét- é àctitiônés ànd éséàcés in té fiélds ôf fôàl étôds ànd sôftwàé énginééing wit té gôàl ôf éxlôiting synégiés ànd futéing ôu undé- stànding ôf séciàlizàtiôn, àbstàctiôn, ànd véificàtiôn técniqués, àông ôté àéàs.

DECLININg DEpENdàbILITy lEvELS Côuté-bàséd systés àé évàsivé ànd nôw influéncé àlôst évéy fàcét ôf ôu livés.Téy wàké us in té ôn- ing, côntôl té côôking ôf ôu fôôd, éntétàin us in té guisé ôf édià lày- és, él in àvôiding tàffic côngéstiôn, côntôl ô idéntify (vià GPS nàvigàtiôn