@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Name: Prover in United Kingdom NP-Tools in Sweden Keywords: automatic proofs, propositional logic, NP-complete, natural deduction, modelling, counter examples Description: Semantics: Propositional logic Deductive machinery: Stalmarck's algorithm Dynamics: Automatically a proof or a counter example is found Persistence: Proof is not saved in current version of the tool (but could be) Contact persons: United Kingdom Graeme I Parkin DITC National Physical Laboratory Queens Road, Teddington, Middlesex United Kingdom, TW11 0LW Tel: +44 181-943 7006 FAX: +44 181-977 7091 email: gip@ditc.npl.co.uk Sweden Gunnar Stalmarck Formal Methods Sweden AB Swedenborgsgatan 2 S-118 48 STOCKHOLM Sweden Tel: +46 8 615 68 60 FAX: +46 8 641 19 06 User group: Publications @INPROCEEDINGS{MFVSSIA, AUTHOR = "{M S\"{a}flund}", TITLE = "{Modelling and Formally Verifying Systems and Software in Industrial Applications}", BOOKTITLE = "{The Second International Conference on Reliability, Maintainability and Safety (ICRMS'94)}", YEAR = "1994" } @ARTICLE{MVSSPL, AUTHOR = "{Gunnar St\aa lmarck and M S\"{a}flund}", TITLE = "{Modelling and Verifying Systems and Software in Propositional Logioc}", JOURNAL = "IFAC SAFECOMP'90", YEAR = "1990", NOTE = "London, UK" } @MISC{FVHSSN, AUTHOR = "{Gunnar St\aa lmarck and Ove \AA kerlund}", TITLE = "{Formal Verification of Hardware and Software Systems using NP-Circuit}", NOTE = "{Reliability and Safety of Processes and Manufacturing Systems, Elsevier Applied Science. Edited by Yngve Malm\'{e}n and Veikko Rouhiainen}", } @MISC{SDPLFAVRTGBF, AUTHOR = "{Gunnar St\aa lmarck}", TITLE = "{System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated from Boolean Formula}", YEAR = "1994", MONTH = "January", NOTE = "{United States Patent. Patent Number 5,276,897. Date of Patent: Jan. 4, 1994}" } Pragmatics: Systems have to be capable of being modelled in propositional logic. Degree of difficulty depends on "hardness" of proof not on size of problem. It has been used to on systems with propositional logic models of over 1 million variables (takes up to 30 -- 60 minutes). Documentation: Manuals come with the tool (at the moment do not tell you how to model systems). Training (including modelling in propositional logic) is available from National Physical Laboratory or Logkkonsult (see contacts above). Applications: Railways -- ABB Signals Prover built into the development lifecycle. Engineers design systems in internal language STERNOL. This is translated into propositional logic. Various properties of system proved. Counter examples are shown in terms of STERNOL. Claims (by ABB Signals) of 30% saving in programming costs and 60% in systems testing costs. Control systems -- Swedish Nuclear Inspectorate Used to verify control systems on nuclear plants. Control systems -- Saab Military Aircraft User to verify systems. Particularly interested in using tool for Fault Tree Analysis (FTA). Notes on the above are contained in the referenced papers. Circuits -- Volvo Analysis of car circuits. Extensions/enhancements: Batch mode Probabilities and Reliability analysis Modal/Temporal Logic Resource requirements: Available on UNIX (SUN, HP) PCs (Windows-NT, Windows 95) MACs (On SUN occupies 7 M bytes of disc space, binary about 3 M bytes) Memory not a problem. Where-to-get-it: See contacts above. Info source, date Graeme I Parkin (see contacts above). 17 August 1995 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%