Tools for VDM in Industry.ppt

1、March 2007,Tools for VDM in Industry,1,Tools for VDM in Industry,Peter Gorm Larsen,March 2007,Tools for VDM in Industry,2,Personal Background,Theoretical Work VDM-SL Semantics (ISO standard) VDM-SL Proof Rules (PhD work) More Practical Work VDM and SA in combination IFAD VDMTools Transfer VDM to Ind

2、ustry Intensive use Industrially Employed by For 13 years: IFAD For 3,5 years: Systematic For 2 years: Engineering College of Aarhus,March 2007,Tools for VDM in Industry,3,Tools for VDM in Industry,IFAD Clients Experiences ”Bootstrapping” VDMTools Overview of VDMTools The Overture/Eclipse Initiative

3、 Vision for the future,March 2007,Tools for VDM in Industry,4,References, World-wide, 2001,France Aerospatiale Espace et Defense Dassault Aviation Dasssault Electronique CISI CEA et Defense CEA Leti Cap Gemini LAAS Matra Bae DynamicsU.K. British Aerospace Systems & Equipment British Aerospace Defens

4、e Adelard ICL Enterprise Engineering Rolls Royce Transitive Technologies,Italy ENEA AnsaldoThe Netherlands Dutch Dept. of Defence Origin ChessPortugal SidereusDenmark Baan Nordic Odense Steel Shipyard DDC International,North America Boeing Rockwell Collins Lockheed Martin DDC-I, Inc. Rational Softwa

5、re Corp. Formal Systems Inc. Concordia UniversityJapan RTRI (Japan Railways) JFITS Felica NetworksGermany GAO mbH,More than 150 VDMTools clients world-wide,March 2007,Tools for VDM in Industry,5,ConForm (1994),Organisation: British Aerospace (UK) Domain: Security (gateway) Tools: The CSK VDM-SL Tool

6、box Experience: Prevented propagation of error Successful technology transfer At least 4 more applications without support Statements: “Engineers can learn the technique in one week” “VDMTools can be integrated gradually into a traditional existing development process”,March 2007,Tools for VDM in In

7、dustry,6,DustExpert (1995-7),Organisation: Adelard (UK) Domain: Safety (dust explosives) Tools: The CSK VDM-SL Toolbox Experience: Delivered on time at expected cost Large VDM-SL specification Testing support valuable Statement: “Using VDMTools we have achieved a productivity and fault density far b

8、etter than industry norms for safety related systems”,March 2007,Tools for VDM in Industry,7,Adelard Metrics,31 faults in Prolog and C+ ( 1/kloc) Most minor, only 1 safety-related 1 (small) design error, rest in coding,March 2007,Tools for VDM in Industry,8,CAVA (1998-),Organisation: Baan (Denmark)

9、Domain: Constraint solver (Sales Configuration) Tools: The CSK VDM-SL Toolbox Experience: Common understanding Faster route to prototype Earlier testing Statement: “VDMTools has been used in order to increase quality and reduce development risks on high complexity products”,March 2007,Tools for VDM

10、in Industry,9,Dutch DoD (1997-8),Organisation: Origin, The Netherlands Domain: Military Tools: The CSK VDM-SL Toolbox Experience: Higher level of assurance Mastering of complexity Delivered at expected cost and on schedule No errors detected in code after delivery Statement: “We chose VDMTools becau

11、se of high demands on maintainability, adaptability and reliability”,March 2007,Tools for VDM in Industry,10,DoD, NL Metrics (1),Estimated 12 C+ loc/h with manual coding!,March 2007,Tools for VDM in Industry,11,DoD - Comparative Metrics,March 2007,Tools for VDM in Industry,12,BPS 1000 (1997-),Organi

12、sation: GAO, Germany Domain: Bank note processing Tools: The CSK VDM-SL Toolbox Experience: Better understanding of sensor data Errors identified in other codeSavings on maintenance Statement: VDMTools provides unparalleled support for design abstraction ensuring quality and control throughout the d

13、evelopment life cycle.,March 2007,Tools for VDM in Industry,13,Flower Auction (1998),Organisation: Chess, The Netherlands Domain: Financial transactions Tools: The CSK VDM+ Toolbox Experience: Successful combination of UML and VDM+ Use iterative process to gain client commitment Implementers did not

14、 even have a VDM course Statement: “The link between VDMTools and Rational Rose is essential for understanding the UML diagrams”,March 2007,Tools for VDM in Industry,14,SPOT 4 (1999),Organisation: CS-CI, France Domain: Space (payload for SPOT4 satellite) Tools: The CSK VDM-SL Toolbox Experience: 38

15、% less lines of source code 36 % less overall effort Use of automatic C+ code generation Statement:The cost of applying Formal methods is significantly lower than without them.,March 2007,Tools for VDM in Industry,15,IFAD VDM Applications,VDMTools VDM interpreter VDM static semantics VDM to C+ code

16、generator Specification manager UML mapper Java static semantics Java VDM+ translatorMUSTER: Emergency response training,March 2007,Tools for VDM in Industry,16,Japanese Railways (2000-2001),Domain: Railways (database and interlocking) Experience: Prototyping important Subsequent also using it for A

17、TC system Engineer working at IFAD for two years,March 2007,Tools for VDM in Industry,17,Stock-options (2000- ),Organisation: JFITS, Japan Domain: Financial Tools: The CSK VDM+ Toolbox Ongoing and still expanding,March 2007,Tools for VDM in Industry,18,Mass producted chicps (2005- ),Organisation: Fe

18、lica Networks (Sony), Japan Domain: Used inside mobile phones Tools: The CSK VDM+ Toolbox Status: Over 100000 lines (677 pages) of VDM+ More than 10 million test cases 110000 lines of C+ in firmware 56 members (did not know FM in advance) Project on schedule (3 years) More than 10 million chips ship

19、ped in 2006 Not a single bug discovered so far,March 2007,Tools for VDM in Industry,19,Further Information,Applying Formal Specification in Industry. P.G. Larsen, J. Fitzgerald and T. Brookes. Published in “IEEE Software“ vol. 13, no. 3, May 1996 A Lightweight Approach to Formal Methods S.Agerholm a

20、nd P.G. Larsen. In Proceedings of the International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, Springer-Verlag, October 1998. Applications of VDM in Banknote Processing P. Smith and P.G. Larsen. + Application of VDM-SL to the Development of the SPOT4 Programming Messages

21、 Generator, A. Puccetti and J.Y. Tixadou + Formal Specification of an Auctioning System Using VDM+ and UML, M.Verhoef et. al.Published at the First VDM Workshop: VDM in Practice with the FM99 Symposium, Toulouse, France, September 1999.,March 2007,Tools for VDM in Industry,20,Tools for VDM in Indust

22、ry,IFAD Clients Experiences ”Bootstrapping” VDMTools Overview of VDMTools The Overture/Eclipse Initiative Vision for the future,March 2007,Tools for VDM in Industry,21,Development Choices Taken,Executable models Testing and animation Partial “analysis” (validation) System level testing Code generati

23、on VDM for source codeFormal refinement and formal verification,March 2007,Tools for VDM in Industry,22,Staff Overview,PGL,PBL,MA,ETN,HC,HV,NK,JNJ,SA,LTO,JWT,OS,JKP,KS,PM,91,92,93,94,95,96,97,98,99,00,NP,MV,KdB,CA,BF,BA,SN,JKP,VS,JKP,WS,JSF,GW,OO,+JR,+ML,+RM,March 2007,Tools for VDM in Industry,23,D

24、evelopment Environment,GNU C+/Visual C+ Generic VDM C+ library GUI: Previously:Tcl/Tk, Now: Qt flex and bison CVS/Ediff version control OSs: Windows, Linux, Unix Test environments Development procedures,March 2007,Tools for VDM in Industry,24,The “Bootstrapping” Process,VDM-SL DS spec,VDM-SL DS impl

25、,Implicit time line,March 2007,Tools for VDM in Industry,25,Specification Sizes,March 2007,Tools for VDM in Industry,26,Component Categories,Purely hand-coded VDM + hand coding VDM + code generation,March 2007,Tools for VDM in Industry,27,Purely Hand-coded Components,Scanner/parser (lex/yacc) pretty

26、-printer (simple C+ component) GUI (previously: Tcl/Tk, now: Qt) Interface to third party tools Rational Rose Corba for API ML for HOL Generic VDM C+ library,March 2007,Tools for VDM in Industry,28,VDM + Hand Coding,Dynamic semantics (SL and +) Static semantics (SL and +) Java/C+ Code generators (SL

27、 and +) Test environments for each component Reused at implementation level Java/C+ code generators now themselves partially code generated,March 2007,Tools for VDM in Industry,29,Maintenance Approach,Bugs first reproduced at specification level Tested using the VDM debugger Check that all tests are

28、 satisfactory Implement changes of specification Rerun all tests at implementation level,March 2007,Tools for VDM in Industry,30,VDM + code generation,Animator for SA/RT Specification Manager (SL and +) VDM+ to/from UML translation Proof support (SL) Parts of GUI now code generated VDM model becomes

29、 source Trade-off with abstraction,March 2007,Tools for VDM in Industry,31,Further Information,An Executable Subset of Meta-IV with Loose Specification, P.G. Larsen, P.B. Lassen, VDM 91: Formal Software Development Methods, 1991 The IFAD VDM-SL Toolbox: A Practical Approach to Formal Specifications,

30、 R. Elmstrm, P.G. Larsen, P.B. Lassen, ACM Sigplan Notices, September 1994 Computer-aided Validation of Formal Specifications, P. Mukherjee, Software Engineering Journal, July 1995 Ten Years of Historical Development - ”Bootstrapping” VDMTools, P.G. Larsen, Journal of Universal Computer Science, 200

31、1,March 2007,Tools for VDM in Industry,32,Tools for VDM in Industry,IFAD Clients Experiences ”Bootstrapping” VDMTools Overview of VDMTools The Overture/Eclipse Initiative Vision for the future,March 2007,Tools for VDM in Industry,33,VDMTools Overview,March 2007,Tools for VDM in Industry,34,Japanese

32、Support via Unicode,March 2007,Tools for VDM in Industry,35,Validation with VDMTools,VDM specs,Test cases,Expected results,Actual results,Comparison,Execution,March 2007,Tools for VDM in Industry,36,Documentation in MS Word/RTF,One compound document:,Documentation Specification Test coverage Test co

33、verage statistics,March 2007,Tools for VDM in Industry,37,Architecture of the Rose VDM+ Link,VDM+ Toolbox,Rational Rose 2000,Class Repository,Class Repository,Merge Tool,VDM+ Files,UML Diagrams,UML model file,March 2007,Tools for VDM in Industry,38,Integrity checker,March 2007,Tools for VDM in Indus

34、try,39,Reference Material,The VDM+ Language for VICE, CSK, 2005 The VDM+ User Manual, CSK, 2005 The VDM+ Installation Guide, CSK, 2005 Rational Rose Link Plug-in Installation and User Guide, CSK, 2005,March 2007,Tools for VDM in Industry,40,Further Information,An Executable Subset of Meta-IV with Lo

35、ose Specification, P.G. Larsen, P.B. Lassen, VDM 91: Formal Software Development Methods, 1991 The IFAD VDM-SL Toolbox: A Practical Approach to Formal Specifications, R. Elmstrm, P.G. Larsen, P.B. Lassen, ACM Sigplan Notices, September 1994 Computer-aided Validation of Formal Specifications, P. Mukh

36、erjee, Software Engineering Journal, July 1995 Ten Years of Historical Development - ”Bootstrapping” VDMTools, P.G. Larsen, Journal of Universal Computer Science, 2001,March 2007,Tools for VDM in Industry,41,Tools for VDM in Industry,IFAD Clients Experiences ”Bootstrapping” VDMTools Overview of VDMT

37、ools The Overture/Eclipse Initiative Vision for the future,March 2007,Tools for VDM in Industry,Overture versus VDMTools,VDMTools (http:/www.vdmtools.jp/en) Closed source, proprietary (available under NDA) Monolithic architecture (single binary), C+ Optimized for performance, industry strength Overt

38、ure Tool project (http:/www.overturetool.org) Open source, GPL license Plug-in architecture, Eclipse, Java Optimized for flexibility, targets academic use (partly) developed using VDMTools,March 2007,Tools for VDM in Industry,43,Overture an open-source initiative,Based on the Eclipse platform Extend

39、ible open VDM+ tool support Initial tool support produced in MSc project in NL MSc project carried out at TUD Jacob Porsborg Nielsen and Jens Kielsgaard Hansen MSc project at Aarhus University Thomas Christensen New MSc projects at Engineering College of Aarhus Hugo Macedo, Minho University Sander V

40、ermolen, University of Nijmegen,March 2007,Tools for VDM in Industry,44,Basic automatic checks and GUI,Overture Architecture Overview,Syntax Check,Type Check,Refactoring support,OML editor With syntax highlighting,Validation support,Pretty Printing With coverage,Interpreter (Debugger) With API capab

41、ilities,Test Generation support,Visualization Support for Execution traces,Verification support,Proof Obligation generation,Automatic Proof support,Interactive Proof support,Model Checking support,Eclipse,AST,Not yet available,Planned,Currently under development,March 2007,Tools for VDM in Industry,

42、Automatic AST generation,OVERTURE AST spec (VDM-SL subset),“implements”,specified in VDM+code generated,other users can use these specs to specify their own OVERTURE extensions (in VDM+),March 2007,Tools for VDM in Industry,Tracefile Viewer (1),March 2007,Tools for VDM in Industry,Tracefile Viewer (

43、2),March 2007,Tools for VDM in Industry,Tracefile Viewer (3),March 2007,Tools for VDM in Industry,49,Tools for VDM in Industry,IFAD Clients Experiences ”Bootstrapping” VDMTools Overview of VDMTools The Overture/Eclipse Initiative Vision for the future,March 2007,Tools for VDM in Industry,50,VDMTools

44、 future,IFAD went bankrupt April 2004 CSK (mother company for JFITS) from Japan bought the IPR for VDMTools from the bankruptcy VDMTools executable and documentation is available again Academic version Non-commercial version Commercial version All freely available! A new book on VDM+ was released Ja

45、nuary 2005,March 2007,Tools for VDM in Industry,51,Extending VDM+ with better support for distributed real-time,Today embedded real-time systems are increasingly distributed Hard to master complexity within tight time schedules Current research work extend VDM+ with better support for describing and

46、 analyzing this Possibility to use CPUs and BUSes inside system Deployment of objects to CPUs Setting priorities of operations Introduction of asynchronous operations Cycles statement in addition to duration statement,March 2007,Tools for VDM in Industry,Combining with continuous time,March 2007,Too

47、ls for VDM in Industry,53,An email from an old (very good) student, At that time I understood that a formal specification would be an advantage for big projects but I had no idea how desperately this is also needed in smaller projects when there are many people involved. Today I do know:At the momen

48、t I am working at BMW in the communications department. We work on the integration of the car telephone (including a telematics unit with GPS coordinates) into the overall car. There is a lot of interaction between the telephone and the HMI of the car and there are different versions and types of al

49、l the involved devices. There are also five companies (BMW, Motorola, Siemens VDO, Harmann-becker, Alpine) who develop the different units. The system should not be so complex because many of the devices should (!) behave similarly. But the specifications we write are English plain text (hundreds of

50、 pages), in our department more than 10 people are involved and we do not know anymore how the devices will behave ourselves.every external company has an own interpretation of the specs and this interpretation changes over time. If you ask the same person twice you get different answers (I frankly admit that I am no exception). You can imagine how “efficient“ everything is and its a miracle that the system still works (with a number of bugs though).,