China
Africa
Explore chapters and articles related to this topic
Software Development Methods and Tools
Published in Paul H. King, Richard C. Fries, Arthur T. Johnson, Design of Biomedical Devices and Systems, 2018
Paul H. King, Richard C. Fries, Arthur T. Johnson
Some of the implementation techniques of formal static analysis include the following: Model checking considers systems that have finite state or may be reduced to finite state by abstractionData flow analysis is a lattice-based technique for gathering information about the possible set of valuesAbstract interpretation models the effect that every statement has on the state of an abstract machine (i.e., it “executes” the software based on the mathematical properties of each statement and declaration). This abstract machine over-approximates the behaviors of the system: the abstract system is thus made simpler to analyze, at the expense of incompleteness (not every property true of the original system is true of the abstract system). If properly done, though, abstract interpretation is sound (every property true of the abstract system can be mapped to a true property of the original system). The Frama-c framework and Polyspace heavily rely on abstract interpretation.Use of assertions in program code as first suggested by Hoare logic. There is tool support for some programming languages (e.g., the SPARK programming language (a subset of Ada) and the Java Modeling Language (JML) using ESC/Java and ESC/Java2, ANSI/ISO C Specification Language for the C language).
Conflict Detection among Multiple Norms in Multi-Agent Systems
Published in Applied Artificial Intelligence, 2018
Eduardo Augusto Silvestre, Viviane Torres da Silva
By considering the execution of Java code annotated with JML, KeY was able to prove the partial correctness of the method by ensuring that the list of actions applied to preconditions implies the postconditions. The Key tool was also able to prove the total correctness of the method by ensuring that the variants in lines 547 and 553 decrease in each iteration of the loop and concluding that the algorithm terminates.