{"entities":{"Q4370601":{"pageid":6400200,"ns":120,"title":"Item:Q4370601","lastrevid":108313865,"modified":"2026-11-05T21:19:36Z","type":"item","id":"Q4370601","labels":{"en":{"language":"en","value":"Proof in VDM. Case studies"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1105197"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4370601$21410861-4F7B-4044-BCA9-F19EA3DD8376","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c707702cb1a654a90482f078141207f71a5ed5ab","datavalue":{"value":"0897.68064","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4370601$577F26CE-BC27-44F0-B7E8-8863595FD3CF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e06ff1cd8e8403fe2fdca2ad132a620003ff250d","datavalue":{"value":{"time":"+1998-01-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4370601$7E7BD8B5-4E4B-4663-B14D-D52361F6FC0E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4370601$0090792E-D2FB-47F7-8A9E-4F3EF2A890E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"24aafcf24a21bd70cd3b62d3f5f72a6d0d82d816","datavalue":{"value":"68-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4370601$0864C1B7-472C-4AF4-BAFA-E35F05306079","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fbea6382513e73774d23db3e9a5d594e06d2a278","datavalue":{"value":"1105197","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4370601$9FBF27D1-D67A-4177-B222-70B9DEB046DE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"94d05492a0435675532bbf6e3f062cf5f6fe0849","datavalue":{"value":"VDM","type":"string"},"datatype":"string"},"type":"statement","id":"Q4370601$F837D5E1-3A34-45EB-8499-99A931EEA0D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"08450ea29c03859f507a60f096c332620f119739","datavalue":{"value":"Case studies","type":"string"},"datatype":"string"},"type":"statement","id":"Q4370601$81BA7A73-6003-4CA7-BEDA-CBBEFBACF007","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"326c300cf62efa849a7bdb94dd90663d744d9f5d","datavalue":{"value":"formal proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q4370601$7F7CB611-2DA5-4B84-B2D8-B420DD5E43B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87994eb840961e5165378eb7f918102952689b42","datavalue":{"value":"formal specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q4370601$E26E00B1-ADC9-4ADF-9518-3BE0C25E82AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9b8eb7d8c3f2086b083c4a6a9925496917122093","datavalue":{"value":"formal model","type":"string"},"datatype":"string"},"type":"statement","id":"Q4370601$43E08897-B1E4-4877-A501-4BA1911584A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1dc9283eec564759c117cc6888635408907541c0","datavalue":{"value":"case study","type":"string"},"datatype":"string"},"type":"statement","id":"Q4370601$61474F96-B47B-4876-9C36-C2F669D363A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"07c02930dc47f6ebf1c2e71be3767111436d61cf","datavalue":{"value":"EXPRESS","type":"string"},"datatype":"string"},"type":"statement","id":"Q4370601$A945527B-0B49-49D1-8226-E7F90232155F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9967a0b50804407b20f63da0231cb5fcf3f7a4e1","datavalue":{"value":"SQL","type":"string"},"datatype":"string"},"type":"statement","id":"Q4370601$68A01DAD-4FA1-476F-A12A-35C5BD033901","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d6de24ac4cac3854a73075b9c4fd4629ef82e8b8","datavalue":{"value":"VDM-SL","type":"string"},"datatype":"string"},"type":"statement","id":"Q4370601$A9879778-E8F7-4378-B981-00D3DEDC7713","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b3d3d0d2409011411be91984a4137a1c90ca04ff","datavalue":{"value":"PVS","type":"string"},"datatype":"string"},"type":"statement","id":"Q4370601$6D2F0FA6-1BAF-4563-B12B-6378355730D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q4370601$4A0237B1-0A81-4F4D-BDDB-687F33F5399F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4370601$7BC7ACAE-31E0-4999-88A2-2FF5C9F32314","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4370601$2703AFE6-BCA1-4737-B33D-44C3B1E65597","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4370601$A2253D36-62D2-4635-8E9B-6327007D4993","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"581279f0ad28c0c70fc3a2b9c99423c9730c6526","datavalue":{"value":{"entity-type":"item","numeric-id":4296956,"id":"Q4296956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"620aed8c92bdedebe43d62cefc3d994c916a29a6","datavalue":{"value":{"amount":"+0.90101963","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4370601$65BB53C2-0F1B-4068-AADF-857ACC59FC5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"59267f35c650dafe313c4eaee81b2b550188f4c2","datavalue":{"value":{"entity-type":"item","numeric-id":4312477,"id":"Q4312477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d89b66a4ed4a8411df67498b2fac208645c1a17e","datavalue":{"value":{"amount":"+0.86804783","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4370601$EF92EA5A-46FC-471F-B04F-9B99FEA170CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"420f00f058046c4352fd747de26d12d7fab8bece","datavalue":{"value":{"entity-type":"item","numeric-id":3809230,"id":"Q3809230"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1d4c857a60aa5992b94fac4318036aebd422b9e7","datavalue":{"value":{"amount":"+0.79506844","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4370601$81466F1D-A0A5-4C88-A73F-D9AA0C358884","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d2a792671d532c04f8515e711fd2637e949af1ca","datavalue":{"value":{"entity-type":"item","numeric-id":3028331,"id":"Q3028331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d724fab29748d03f4ee7931a2ad274336e80e602","datavalue":{"value":{"amount":"+0.79458576","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4370601$DB74D4FF-7301-4B5E-A517-9BE769A6657C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"de595cb0f5fc164a936fed0b166678d13dc24ca2","datavalue":{"value":{"entity-type":"item","numeric-id":3336731,"id":"Q3336731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"09e0c481a25b2aa7b871856928e85fd2216249dd","datavalue":{"value":{"amount":"+0.78955585","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4370601$0169C7F9-90E8-44C5-8B37-C3F2DD5B46E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f783adefd14c19385f04542db3af561e5b30f6c4","datavalue":{"value":{"entity-type":"item","numeric-id":5284601,"id":"Q5284601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c8b5e635ffd82079bfda94c76da9a66476ebf371","datavalue":{"value":{"amount":"+0.78249204","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4370601$13F3986A-659D-41FF-9BA6-7F2C40D16E7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"94eeed2907d2dd6f99b42b155742fe44148d4ba6","datavalue":{"value":{"entity-type":"item","numeric-id":5747656,"id":"Q5747656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4440fb170738055e7e031e83d43e3fb56bb75216","datavalue":{"value":{"amount":"+0.7803089","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4370601$726A94F1-84A5-4A64-9123-E610AC0261FA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f292d89367c8a466f1df2adeac5cd6b8a82670f2","datavalue":{"value":{"text":"Proof in VDM. Case studies","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4370601$21D10AA7-7F3D-4016-A0C1-F60235D84660","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"5085a8576e74806b9e3c146ab86bf39c7d9a736c","datavalue":{"value":"This book describes a collection of case studies in the use of formal and rigorous proof in the validation and verification of formal specifications. Being a continuation of an earlier book [\\textit{J.C. Bicarregui} et al., Proof in VDM: A Practitioner's Guide (1994; Zbl 0809.68023)], this book presents the use of the techniques described in the first book, in a range of actual applications. The book contains seven chapters. The first four chapters describe some case studies based on various proofs developed by hand. The remaining chapters focus on different support tools. The case study described in the first chapter deals with a formal model of a nuclear process tracking system. It illustrates the main issues arising as part of the proof based analysis of the specification for that system. The formal model, the elicitation and formalisation of safety properties from the model, as well as the proof that the model is consistent with respect to these properties are presented. The second case study deals with proving the properties of an existing specification - a model of UN regulations for safe storage of explosives-. In particular it is described the proof of satisfiability of an operation from the specification and the proof of the correctness of a specification modification. The third chapter presents a case study concerning the specification and validation of a Security Policy Model (SPM) for an electronic network supporting multiple levels of security classification. The SPM is formally specified in VDM-SL and validated by showing that the model is mathematically consistent and satisfies some security properties. The fourth chapter describes the specification and proof of an EXPRESS to SQL compiler. An abstract specification of an EXPRESS database is given and the corresponding concrete version of the implementation on top of a SQL relational database is refined. The fifth chapter presents a unified formalisation of shared memory models for explicitly parallel programs. The Mural tool was used for writing the VDM specification and generating the corresponding formal theory and constructing some formal proofs of basic properties of the model. The sixth chapter describes the use of the PVS system to support proof in VDM. It is described a translation from VDM-SL into PVS specification language. It is also presented the use of PVS for type checking and verifying properties of VDM-SL specifications and refinements. The last chapter describes the construction of a theorem proving component of a prototype integrated CASE and theorem proving tool which combines the benefits of the general-purpose theorem prover, called Isabelle, with those of a commercial software development environment for VDM-SL, called IFAD VDM-SL Toolbox. The book will be of value for those being interested in formal methods, in writing formal specifications and in constructing proofs about them.","type":"string"},"datatype":"string"},"type":"statement","id":"Q4370601$DA586CBA-8D0A-43B8-96EC-514F61975977","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proof in VDM. Case studies","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Proof_in_VDM._Case_studies"}}}}}