kprasad@caip.rutgers.edu (K. Venkatesh Prasad) (04/06/91)
Are there companies in the United States that are using formal methods for specifying and verifying software? -- K. Venkatesh Prasad Machine Vision Group
markh@csd4.csd.uwm.edu (Mark William Hopkins) (04/17/91)
In article <Apr.5.16.43.23.1991.13165@caip.rutgers.edu> kprasad@caip.rutgers.edu (K. Venkatesh Prasad) writes: >Are there companies in the United States that are using >formal methods for specifying and verifying software? I use formal methods to both derive and verify software for my business. Our more recent development involved converting a single controller into a virtual 2-thread threaded controller using the Product Construction listed in your typical Automata textbook. Another method used for verifying assembly involved developing a mathematical model of a multiprocessing architecture, reverse translating the assembly to C (I usually write assembly by first specifying it in C), and verifying the result on the model. To verify C programs (or programs in any imperative language), I usually partially or completely convert parts of all of the program into something much like a Recursive Transition Network. The mathematical tools are then basically the algebraic tools of formal language theory. Usually you don't need to go all the way. It's sometimes sufficient to just use the underlying control-flow state automaton and do mathematical manipulations on that. Loops I can often convert to diophantine equations whose solutions leads ultimately to the semantics of the loop in question. Most of the verification for multiprocessing, and interrupts in controllers centers around proving that all time conflicts and register or memory use conflicts are resolved appropriately (that is, after each of the processes has been verified individually). A good run or two of the software (during testing) will also help spur the wheels of mathematical induction by providing a good concrete basis to work off of. And oftentimes, a simple test can reveal a flaw a lot quicker than textual analysis. So the two get used in parallel. Typical applications involve source-optimizing control structures, and variable usage and verifying assertions made about the variables or routines in the program. Specifications are never made in completion in advance. Instead, they will usually consist of a list of "to-do"'s: things that need to happen before the software is considered valid. Whatever else is there or not there is irrelevant (until it becomes relevant, in which case we add a new item to the to-do list). So verification just means exhausting the to-do list by formal methods. It definitely does NOT mean proving the equivalence of written software to another piece of software going under the name of "specification" written in some abstract language. That's unnecessary.