Multitude Corporation was founded by Brian R Larson to make a new kind of supercomputer with a novel model of computation. This was patented a DANCE/Multitude Concurrent Computation Pat. No. 5,867,649. The language Declarative Axiomatic Notation for Concurrent Execution provided temporal logic formulas satisfied by lattices of states. A lattice is a kind of directed graph which is acyclic having a “start” state having paths to all other states in the graph, and an “end” state which is reachable from all other states in the graph. A lattice defines a partial order: if a path exists from one state to another, it must occur “before” that state; if no path exists between states, they may occur in either order or concurrently. Short, broad lattices provided many opportunities for concurrent execution. A sequence is a lattice with no opportunity for concurrent execution.
DANCE programs allowed non-executed first-order predicates to be interspersed throughout the temporal logic formulas to be “proof outlines” inspired by the guarded commands language expounded in The Science of Programming. Originally, DANCE program proof outlines were manually inspected, like a mathematical proof, to determine whether they were convincing (correct). The logic of proofs was “higher order” because its domain was triples of logic formulas: first-order predicates applied to the values of variables in start and end states of a lattice, and a temporal logic formula when satisfied would “compute” the end state from the start state. Higher-order logics were believed to be intractable.
Discussions with Gopalan Nadathur at the University of Minnesota, and reading his papers on higher-order logics made them seem less daunting, and inspired creation of the DANCE Proof Assistant to transform DANCE program proof outlines into deductive proofs: sequences of theorems either given or axiomatic, or derived from prior theorems by stated inference rules, the last of which stated that all possible computations starting with its precondition being true would terminate with its postcondition being true. Unfortunately, Multitude Corporation was unable to attract enough venture capital to build a prototype to show significantly better speedup than replicated, sequential control flow architecture, and the rejection of Multitude Corporation’s proposal for DARPA’s High End Computing and Computation program terminated supercomputing efforts.
Thereafter, Mr. Larson began a Systems Engineering job at Guidant (later Boston Scientific) Cardiac Rhythm Management. Inspired by Guidant’s commitment to excellence and quality, Mr. Larson began thinking about how to apply DANCE program correctness proofs to pacemakers and implantable cardio-defibrillators. Guidant pioneered design of medical devices using a (proprietary) architecture description language derived from Honeywell’s MetaH. Learning that SAE International had standardized their Architecture Analysis and Design Language (AADL version 1), also derived from MetaH, Mr. Larson took an AADL tutorial at the Software Engineering Institute (SEI), at which he was invited to join the AADL Standard Committee.
AADL has a core language defining system structure, which is extensible by properties and annex sublanguages. When the AADL Standard Committee considered a behavior annex sublanguage (which became known as “BA”), Mr. Larson thought it could be augmented with predicates to be proof outlines which could be transformed into deductive proofs with the DANCE Proof Assistant. BA defined state-transition machines wherein transitions had source and destination states, a transition condition which must be true for the transition to be taken, and an optional action performed after leaving the source state, before entering the destination state. If states had predicates expressing what was true about the system when in that state, the conjunction of source state’s predicate and the transition condition could be the precondition of the action, and the destination state’s predicate could be the postcondition.
Thus BLESS was born as BA augmented with non-executed predicates to be proof outlines, and the DANCE Proof Assistant adapted to transform BLESS program proof outlines into proofs. The BLESS Proof Assistant still uses Java code from the original DANCE Proof Assistant.
After leaving Boston Scientific (having acquired Guidant), Mr. Larson worked with John Hatcliff at Kansas State University under the US National Science Foundation/Food and Drug Administration Scholar in Residence program for several years. Despite lapse of funding they continue to collaborate on academic papers and High-Assurance Modeling and Rapid Engineering for Embedded Systems (HAMR) tool suite to generate executable, deployable code from proved-correct BLESS programs.