formal methods in computer science specifically software engineering and hardware engineering formal methods are a particular kind of mathematically based technique for the specification development and verification of software and hardware systems formal methods are best described as the application of a fairly broad variety of theoretical computer science fundamentals in particular logic calculi formal languages automata theory discrete event dynamic system and program semantics but also type systems and algebraic data types to problems in software and hardware specification and verification taxonomy formal methods can be used at a number of levels level 0 formal specification may be undertaken and then a program developed from this informally this has been dubbed formal methods lite this may be the most costeffective option in many cases level 1 formal development and formal verification may be used to produce a program in a more formal manner for example proofs of properties or refinement from the specification to a program may be undertaken this may be most appropriate in highintegrity systems involving safety or security level 2 theorem provers may be used to undertake fully formal machinechecked proofs this can be very expensive and is only practically worthwhile if the cost of mistakes is extremely high eg in critical parts of microprocessor design further information on this is expanded below as with programming language semantics styles of formal methods may be roughly classified as follows denotational semantics in which the meaning of a system is expressed in the mathematical theory of domains proponents of such methods rely on the wellunderstood nature of domains to give meaning to the system critics point out that not every system may be intuitively or naturally viewed as a function operational semantics in which the meaning of a system is expressed as a sequence of actions of a presumably simpler computational model proponents of such methods point to the simplicity of their models as a means to expressive clarity critics counter that the problem of semantics has just been delayed who defines the semantics of the simpler model axiomatic semantics in which the meaning of the system is expressed in terms of preconditions and postconditions which are true before and after the system performs a task respectively proponents note the connection to classical logic critics note that such semantics never really describe what a system does merely what is true before and afterwards lightweight formal methods some practitioners believe that the formal methods community has overemphasized full formalization of a specification or design uses formal methods can be applied at various points through the development process specification formal methods may be used to give a description of the system to be developed at whatever levels of detail desired this formal description can be used to guide further development activities see following sections additionally it can be used to verify that the requirements for the system being developed have been completely and accurately specified the need for formal specification systems has been noted for years in the algol 58 report backus also wrote that a formal description of the meaning of syntactically valid algol programs wasnt completed in time for inclusion in the report therefore the formal treatment of the semantics of legal programs will be included in a subsequent paper it never appeared development once a formal specification has been produced the specification may be used as a guide while the concrete system is developed during the design process ie realized typically in software but also potentially in hardware for example if the formal specification is in an operational semantics the observed behavior of the concrete system can be compared with the behavior of the specification which itself should be executable or simulateable additionally the operational commands of the specification may be amenable to direct translation into executable code if the formal specification is in an axiomatic semantics the preconditions and postconditions of the specification may become assertions in the executable code verification once a formal specification has been developed the specification may be used as the basis for proving properties of the specification and hopefully by inference the developed system humandirected proof sometimes the motivation for proving the correctness of a system is not the obvious need for reassurance of the correctness of the system but a desire to understand the system better consequently some proofs of correctness are produced in the style of mathematical proof handwritten or typeset using natural language using a level of informality common to such proofs a good proof is one which is readable and understandable by other human readers critics of such approaches point out that the ambiguity inherent in natural language allows errors to be undetected in such proofs often subtle errors can be present in the lowlevel details typically overlooked by such proofs additionally the work involved in producing such a good proof requires a high level of mathematical sophistication and expertise automated proof in contrast there is increasing interest in producing proofs of correctness of such systems by automated means automated techniques fall into three general categories automated theorem proving in which a system attempts to produce a formal proof from scratch given a description of the system a set of logical axioms and a set of inference rules model checking in which a system verifies certain properties by means of an exhaustive search of all possible states that a system could enter during its execution abstract interpretation in which a system verifies an overapproximation of a behavioural property of the program using a fixpoint computation over a possibly complete lattice representing it some automated theorem provers require guidance as to which properties are interesting enough to pursue while others work without human intervention model checkers can quickly get bogged down in checking millions of uninteresting states if not given a sufficiently abstract model proponents of such systems argue that the results have greater mathematical certainty than humanproduced proofs since all the tedious details have been algorithmically verified the training required to use such systems is also less than that required to produce good mathematical proofs by hand making the techniques accessible to a wider variety of practitioners critics note that some of those systems are like oracles they make a pronouncement of truth yet give no explanation of that truth there is also the problem of verifying the verifier if the program which aids in the verification is itself unproven there may be reason to doubt the soundness of the produced results some modern model checking tools produce a proof log detailing each step in their proof making it possible to perform given suitable tools independent verification the main feature of the abstract interpretation approach is that it provides a sound analysis ie no false negatives are returned moreover it is efficiently scalable by tuning the abstract domain representing the property to be analyzed and by applying widening operators to get fast convergence applications formal methods are applied in different areas of hardware and software including routers ethernet switches routing protocols and security applications there are several examples in which they have been used to verify the functionality of the hardware and software used in dcs there are several other projects of nasa in which formal methods are applied such as next generation air transportation system bmethod with atelierb is used to develop safety automatisms for the various subways installed throughout the world by alstom and siemens and also for common criteria certification and the development of system models by atmel and stmicroelectronics formal verification has been frequently used in hardware by most of the wellknown hardware vendors such as ibm intel and amd there are many areas of hardware where intel have used fms to verify the working of the products such as parameterized verification of cache coherent protocol in software development in software development formal methods are mathematical approaches to solving software and hardware problems at the requirements specification and design levels formal methods are most likely to be applied to safetycritical or securitycritical software and systems such as avionics software software safety assurance standards such as do178b do178c and common criteria demand formal methods at the highest levels of categorization for sequential software examples of formal methods include the bmethod the specification languages used in automated theorem proving raise and the z notation in functional programming propertybased testing has allowed the mathematical specification and testing if not exhaustive testing of the expected behaviour of individual functions the object constraint language and specializations such as java modeling language has allowed objectoriented systems to be formally specified if not necessarily formally verified for concurrent software and systems petri nets process algebra and finite state machines which are based on automata theory see also virtual finite state machine or event driven finite state machine allow executable software specification and can be used to build up and validate application behavior another approach to formal methods in software development is to write a specification in some form of logicusually a variation of firstorder logic foland then to directly execute the logic as though it were a program the owl language based on description logic dl is an example there is also work on mapping some version of english or another natural language automatically to and from logic and executing the logic directly examples are attempto controlled english and internet business logic which do not seek to control the vocabulary or syntax a feature of systems that support bidirectional englishlogic mapping and direct execution of the logic is that they can be made to explain their results in english at the business or scientific level formal methods and notations there are a variety of formal methods and notations available specification languages abstract state machines asms a computational logic for applicative common lisp acl2 ansiiso c specification language acsl alloy autonomic system specification language assl bmethod cadp common algebraic specification language casl java modeling language jml knowledge based software assistant kbsa process calculi csp lotos calculus actor model esterel lustre mcrl2 perfect developer petri nets predicative programming raise rebeca modeling language spark ada spec sharp spec specification and description language tla usl vdm vdmsl vdm z notation model checkers spin pat is a powerful free model checker simulator and refinement checker for concurrent systems and csp extensions eg shared variables arrays fairness malpas software static analysis toolset is an industrial strength model checker used for formal proof of safetycritical systems uppaal esbmc abstract interpretation automated theorem proving design by contract formal methods people formal specification formal verification formal system model checking software engineering specification language this article is based on material taken from the free online dictionary of computing prior to 1 november 2008 and incorporated under the relicensing terms of the gfdl version 13 or later jean franois monin and michael g hinchey understanding formal methods springer 2003 isbn1852332476 jonathan p bowen and michael g hinchey formal methods in allen b tucker jr ed computer science handbook 2nd edition section xi software engineering chapter 106 pages 1061 10625 chapman hall crc press association for computing machinery 2004 michael g hinchey jonathan p bowen and emil vassev formal methods in philip a laplante ed encyclopedia of software engineering taylor francis 2010 pages 308320 hubert garavel editor and susanne graf formal methods for safe and secure computer systems bundesamt fr sicherheit in der informationstechnik bsi study 875 bonn germany 362 pages december 2013 formal methods europe fme formal method keyword on microsoft academic search foldocformal methods evidence on formal methods uses and impact on industry supported by the deploy project eu fp7 vtemajor fields of computer sciencenote this template roughly follows the 2012 acm computing classification systemhardware printed circuit board peripheral integrated circuit very large scale integration systems on chip socs energy consumption green computing electronic design automation hardware acceleration computer systemsorganization computer architecture embedded system realtime computing dependability networks network architecture network protocol network components network scheduler network performance evaluation network service software organization interpreter middleware virtual machine operating system software quality software notationsand tools programming paradigm programming language compiler domainspecific language modeling language software framework integrated development environment software configuration management software library software repository software development software development process requirements analysis software design software construction software deployment software maintenance programming team opensource model theory of computation model of computation formal language automata theory computational complexity theory logic semantics algorithms algorithm design analysis of algorithms algorithmic efficiency randomized algorithm computational geometry mathematicsof computing discrete mathematics probability statistics mathematical software information theory mathematical analysis numerical analysis informationsystems database management system information storage systems enterprise information system social information systems geographic information system decision support system process control system multimedia information system data mining digital library computing platform digital marketing world wide web information retrieval security cryptography formal methods security services intrusion detection system hardware security network security information security application security humancomputerinteraction interaction design social computing ubiquitous computing visualization accessibility concurrency concurrent computing parallel computing distributed computing multithreading multiprocessing artificialintelligence natural language processing knowledge representation and reasoning computer vision automated planning and scheduling search methodology control method philosophy of artificial intelligence distributed artificial intelligence machine learning supervised learning unsupervised learning reinforcement learning multitask learning crossvalidation graphics animation rendering image manipulation graphics processing unit mixed reality virtual reality image compression solid modeling appliedcomputing ecommerce enterprise software computational mathematics computational physics computational chemistry computational biology computational social science computational engineering computational healthcare digital art electronic publishing cyberwarfare electronic voting video games word processing operations research educational technology document management book category portal wikiproject commons vtesoftware engineeringfields computer programming requirements engineering software deployment software design software maintenance software testing systems analysis formal methods concepts data modeling enterprise architecture functional specification modeling language orthogonality programming paradigm software software archaeology software architecture software configuration management software development methodology software development process software quality software quality assurance software verification and validation structured analysis orientations agile aspectoriented object orientation ontology service orientation sdlc modelsdevelopmental agile eup executable uml incremental model iterative model prototype model rad up scrum spiral model vmodel waterfall model xp other spice cmmi data model er model function model information model metamodeling object model systems model view model languages idef uml usl sysml softwareengineers victor basili kent beck grady booch fred brooks barry boehm peter chen danese cooper ward cunningham tom demarco edsger w dijkstra delores m etter martin fowler adele goldstine margaret hamilton c a r hoare lois haibt mary jean harrold grace hopper watts humphrey michael a jackson ivar jacobson alan kay nancy leveson stephen j mellor bertrand meyer david parnas trygve reenskaug winston w royce james rumbaugh mary shaw peri tarr elaine weyuker niklaus wirth edward yourdon related fields computer science computer engineering project management risk management systems engineering category commons 