You are currently browsing the category archive for the ‘SimulationWare’ category.
In computer science, symbolic execution (also symbolic evaluation) refers to the analysis of programs by tracking symbolic rather than actual values, a case of abstract interpretation. The field of symbolic simulation applies the same concept to hardware. Symbolic computation applies the concept to the analysis of mathematical expressions.
Symbolic execution is used to reason about all the inputs that take the same path through a program.
Symbolic execution is useful for software testing because it can analyse if and when errors in the code may occur. It can be used to predict what code statements do to specified inputs and outputs. It is also important for considering path traversal.
Symbolic execution is used to reason about a program pathbypath. This may be superior to reasoning about a program, like Dynamic program analysis does, inputbyinput.
Symbolic execution vs Symbolic Analysis (Laitila, 2008)
Symbolic execution emphasizes execution, travering program paths. Symbolic analysis has the same purpose, but furthermore, it is a formalism to run / execute symbols using their internal state automaton. The automaton can be programmed to do anything, which is characteristics for the symbol. One exellent feature of symbolic analysis is its reduncancy and the internal semantics of each symbol because of its clausenotation in the Symboliclanguage. It is possible to reconstruate parse trees from the symbols so that the side effects caused by any symbol can be matched with the corresponding symbols. This makes it possible to partially verify the code.
Some links:
 Symbolic Execution at Wiki: http://en.wikipedia.org/wiki/Symbolic_execution
Executable UML, often abbreviated to xtUML or xUML, is the evolution of the ShlaerMellor method to UML. Executable UML graphically specifies a system using a profile of the UML. The models are testable, and can be compiled into a less abstract programming language to target a specific implementation. Executable UML supports MDA through specification of platformindependent models, and the compilation of the platformindependent models into platformspecific models.
Executable UML is used to model the domains in a system. Each domain is defined at the level of abstraction of its subject matter independent of implementation concerns. The resulting system view is composed of a set of models represented by at least the following:
 The domain chart provides a view of the domains in the system, and the dependencies between the domains.
 The class diagram defines the classes and class associations for a domain.
 The statechart diagram defines the states, events, and state transitions for a class or class instance.
 The action language defines the actions or operations that perform processing on model elements.
Shortcomings of Executable UML
UML doesn’t define semantics of a programming language. Hence, it is not complete to describe behavior of any exact system. In order to correct this shortcoming some new principles are needed. Some of them are: automata theory and symboldriven engineering.
Automata Theory and SymbolDriven Engineering (SDE)
Automata theory defines behavior model for corresponding code elements. Therefore, this theory background eliminates the gap between program behavior and the corresponding model, like UML
In SDE every symbol has an automaton behind it. In order to execute those symbols an invocation Symbol:run is needed plus some specific initailizations for some specific symbols like definitions (method invocations and object and variable definitions). See figure below.
Some links:

^{ Book: }^{ } Mellor, S; Balcer, M: “Executable UML: A foundation for modeldriven architecture”, Preface, Addison Wesley, 2002
 Wiki: http://en.wikipedia.org/wiki/Executable_UML
In computer programming, program slicing is the computation of a program slice. The program slice consists of the parts of a program that may affect the values computed at some point of interest, referred to as a slicing criterion. Program slicing can be used in debugging to locate source of errors more easily. Other applications of slicing include software maintenance, optimization, program analysis, and information flow control.
Slicing techniques have been seeing a rapid development since the original definition by Mark Weiser. At first, slicing was only static, i.e., applied on the source code with no other information than the source code. Bogdan Korel and Janusz Laski introduced dynamic slicing, which works on a specific execution of the program (for a given execution trace). Other forms of slicing exist, for instance path slicing.
Slicing in Symbolic Analysis
Symbolic analysis is a method to traverse source code symbols by using a specific traversing algorithm, or by simulating the corresponding code. Actually symbolic analysis is static slicing, but it tries to mimich dynamic behavior, too. As an output of simulation symbolic analysis creates side effect elements, which are execution results from symbols.
Below a rough principle about a slice generated from symbolic analysis.
Some links:
Gödel’s incompleteness theorems are two theorems of mathematical logic that state inherent limitations of all but the most trivial axiomatic systems for arithmetic.
Gödel’s first incompleteness theorem states that:
Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true,^{[1]} but not provable in the theory (Kleene 1967).
The liar paradox is the sentence “This sentence is false.
Gödel’s second incompleteness theorem can be stated as follows:
For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, T includes a statement of its own consistency if and only if T is inconsistent.
Arithmetization of syntax
The main problem in fleshing out the proof described above is that it seems at first that to construct a statement p that is equivalent to “p cannot be proved”, p would have to somehow contain a reference to p, which could easily give rise to an infinite regress. Gödel’s ingenious trick, which was later used by Alan Turing in his work on the Entscheidungsproblem, is to represent statements as numbers, which is often called the arithmetization of syntax. This allows a selfreferential formula to be constructed in a way that avoids any infinite regress of definitions.
To begin with, every formula or statement that can be formulated in our system gets a unique number, called its Gödel number. This is done in such a way that it is easy to mechanically convert back and forth between formulas and Gödel numbers. It is similar, for example, to the way English sentences are encoded as sequences (or “strings”) of numbers using ASCII: such a sequence is considered as a single (if potentially very large) number. Because our system is strong enough to reason about numbers, it is now also possible to reason about formulas within the system.
A formula F(x) that contains exactly one free variable x is called a statement form or classsign. As soon as x is replaced by a specific number, the statement form turns into a bona fide statement, and it is then either provable in the system, or not. For certain formulas one can show that for every natural number n, F(n) is true if and only if it can be proven (the precise requirement in the original proof is weaker, but for the proof sketch this will suffice). In particular, this is true for every specific arithmetic operation between a finite number of natural numbers, such as “2*3=6”.
Statement forms themselves are not statements and therefore cannot be proved or disproved. But every statement form F(x) can be assigned with a Gödel number which we will denote by G(F). The choice of the free variable used in the form F(x) is not relevant to the assignment of the Gödel number G(F).
Now comes the trick: The notion of provability itself can also be encoded by Gödel numbers, in the following way. Since a proof is a list of statements which obey certain rules, we can define the Gödel number of a proof. Now, for every statement p, we may ask whether a number x is the Gödel number of its proof. The relation between the Gödel number of p and x, the Gödel number of its proof, is an arithmetical relation between two numbers. Therefore there is a statement form Bew(x) that uses this arithmetical relation to state that a Gödel number of a proof of x exists:
Bew(y) = ∃ x ( y is the Gödel number of a formula and x is the Gödel number of a proof of the formula encoded by y).
The name Bew means provable ( German word) . An important feature of the formula Bew(y) is that if a statement p is provable in the system then Bew(G(p)) is also provable. This is because any proof of p would have a corresponding Gödel number, the existence of which causes Bew(G(p)) to be satisfied.
Prolog creates Gödel numbers
Prolog’s type system uses Gödel numbers internally. Prolog uses the resolution theorem (by John Alan Robinson) for showing which clauses are satifsfiable.
In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theoremproving technique for sentences in propositional logic and firstorder logic. In other words, iteratively applying the resolution rule in a suitable way allows for telling whether a propositional formula is satisfiable and for proving that a firstorder formula is unsatisfiable. This method may prove the satisfiability of a firstorder satisfiable formula, but not always, as it is the case for all methods for firstorder logic.
The relation of the symbolic atomistic model for proving software and the incompleteness theorems
The atomistic model simulates code symbols as an automaton each. The output of the simulated clauses (side effcts) is not complete as itself, but it allows the user to find possible contradictions or logical errors in the code by connecting the symbols that are causing side effects the the output states (the side effect elements).
Some links:
A Kripke structure is a type of nondeterministic finite state machine used in model checking to represent the behaviour of a system. It is basically a graph whose nodes represent the reachable states of the system and whose edges represent state transitions. A labeling function maps each node to a set of properties that hold in the corresponding state. Temporal logics are traditionally interpreted in terms of Kripke structures.
Let AP be a set of atomic propositions, i.e. boolean expressions over variables, constants and predicate symbols.
A Kripke structure is a 4tuple consisting of
 a finite set of states
 a set of initial states
 a transition relation where such that
 a labeling (or interpretation) function
Since R is lefttotal, it is always possible to construct an infinite path through the Kripke structure. Thus a deadlock state has a single outgoing edge back to itself.
The labeling function L defines for each state s ∈ S the set L(s) of all atomic propositions that are valid in s. In the Kripke structure, the transition function should be complete,i.e each and every state should have transition.In other words there should not be any dead states in the graph.
Combining the Semantics of the Atomistic Model and the Kripke Structure with each other
If we use the notation of the Kripke structure for the Atomistic Model we get the definitions:
The atomistic model is a Kripke structure, a 4tuple consisting of
 a finite set of states implemented as symbols in the model illustrating clauses of the original clause and side effects caused by the simulation/evaluation processes.
 a set of initial states implemented as symbols of the models: either clauses or side effects.
 a transition relation where such that implemented as links of the symbols.
 a labeling (or interpretation) function implemented as a commandfact in each symbol.
Summary about the correspondece
The atomistic model is downwards compatible with the Kripke structure. It leads to a conculsion (by inspection) that all functions and mathematical processes intended for the Kripke structure, e.g. model checking, can be borrowed for the use of the atomistic model. Only a simple transformation is needed.
Some links:
Understanding side effects is one of the most complex and challenging things of program comprehension.
In computer science, a function or expression or method or class or a package is said to have a side effect if, in addition to producing a value, it also modifies some state or has an observable interaction with calling functions or the outside world. For example, a function might modify a global or a static variable, modify one of its arguments, raise an exception, write data to a display or file, read data, or call other sideeffecting functions. In the presence of side effects, a program’s behavior depends on history; that is, the order of evaluation matters. Because understanding an effectful program requires thinking about all possible histories, side effects often make a program harder to understand.
Side effects are essential to enable a program to interact with the outside world (people, filesystems, other computers on networks). But the degree to which side effects are used depends on the programming paradigm. Imperative programming is known for uncontrolled, promiscuous use of side effects. Thus, the languages Java, C++ and other imperative ones are problematic referring to the scope of this title.
How side effects can be captured in the analyzing paradigms
 Static analysis cannot handle side effects, at all.
 For dynamic analysis, selected clauses can be stored into a trace or an output.
 For symbolic analysis (Laitila), every activity for every symbol can be traced and stored, if needed.
The output of symbolic analysis is the most accurate trace
If symbol S activates symbol S1 in order to evaluate whether it is true or not, an side effect symbol SE1 can be created every time when S1 is evaluated. Hence, after execution the output trace is S • S1 • SE1.
That ifcondition was only one small example, but by extending the same principle for any statement and for any evaluation, it is possible to get detailed information about complex algorithms and separated threads, almost any typical clause of the code. However, there are some restrictions about whether it is possible to evaluate a statement (clause) or not. See more about computability conditions.
Summary about side effects
Symbolic analysis is the most accurate paradigm to save evaluation results: all or selectively any category of computations.
By using side effect elements it is possible for the user, to verify some specific parts of the program, piece by piece, if only it is possible for him/her to formulate the necessary input preconditons (prerequisities) for the code. In some cases verifying program parts is still rather challenging manually. In those cases, it is recommended to load the output(s) of the symbolic analysis into any commercial or free graph tool, e.g. pert graph tool, a visualization tool, Excel or similar. Those generic tools are helpful in finding anomalies or general rules based on the symbols and side effects.
Universal Turing machine (UTM) is a Turing machine that can simulate an arbitrary Turing machine on arbitrary input. The universal machine essentially achieves this by reading both the description of machine to be simulated as well as the input thereof from its own tape. This model is considered by some to be the origin of the stored program computer—used by John von Neumann for the “Electronic Computing Instrument” that now bears von Neumann’s name: the von Neumann architecture.
Universal machine is also known as universal computing machine, universal machine, machine U, U.
Alan Turing described his construction in complete detail in his 1936 paper:
 “It is possible to invent a single machine which can be used to compute any computable sequence. If this machine U is supplied with a tape on the beginning of which is written the S.D [“standard description” of an action table] of some computing machine M, then U will compute the same sequence as M.
Universal Turing Machine uses numbers in its tape as input and as output. Its commands are Left, Right and Skip.
Symbolic Abstract Machine (SAM) compared with UTM
SAM differs from UTM, because it can use higher abstraction symbols as its input and output. The logic for each symbol is written into the symbol: the commandfact. By applying these two modifications it is possible to create a higher abstraction UTM, which is capable of simulating typical programming languages.
We can describe our novel construction in complete detail:
 “It is possible to invent a single machine which can be used to compute any computable sequence using programming language semantics. If this machine SAM is supplied with a tape on the beginning of which is written the S.D [“standard description” of an action table] of some computing machine M, then SAM will compute the same sequence as M.”
 If we thing each symbol to work like an atomic formula, only containing one reductionist formula, the construction of a symbol resembles the one of the metaphor of an atom. Hence, our SAM works using atoms, each atom containing an automaton, in the way that UTM has.
Some links:
 UTM: http://en.wikipedia.org/wiki/Universal_Turing_machine

Symbolic Hybrid Programming Tool for Software Understanding. 3rd Int. Workshop on Hybrid Artificial Intelligence Systems. HAIS’2008, Burgos, Spain, Springer LNAI 5271, pp. 499506.
 Symbolic Hybrid Programming Tool: http://www.springerlink.com/content/a857w8311620x57j/
There are two types of model checking: explicit state and symbolic model checking. We suggest symbolic analysis as an alternative for focused verification, a novel paradigm with a simulation capability.
Explicit State Model Checking
 states are enumerated onthefly
 Forwards analysis
 Stores visited states in a hashtable
 Memory intensive
 Good for finding concurrency errors
 Short execution paths are better, but long execution paths can also be handled
 Can handle dynamic creation of objects/threads
 Mostly used in software
Symbolic Model Checking
 Sets of states are manipulated at a time
 Typically a backwards analysis
 Transition relation encoded by (some variant of) Binary Decision Diagrams (BDDs) or as a satisfiability problem
 Can handle very large state spaces
 Not as good for asynchronous systems
 Cannot deal well with long execution traces
 Works best with a static transition relation, hence doesn’t deal well with dynamic creation of objects/threads
 Mostly used in hardware
How symbolic analysis differs from Symbolic and Explicit Model Checking?
Atomistic model and symbolic analysis, presented in this blog do not provide any complete model checking strategy. Instead, symbolic analysis provides a simulation methodology (SimulationWare), which estimates one use scenario of the code at a time. By repeating numerous scenarios it is possible for the user to evaluate alternative paths, but the purpose of it is not automatic proving, complete verification, but proving partial correctness in cooperation with the tool and the user. The characteristics of symbolic analysis are:
 Focused approach, not holistic
 Symbolic execution traces. It is possible to use these outputs for verification purposes.
 Mostly used for troubleshooting purposes
 States are modeled using side effect elements (internal state variables)
 Formwards analysis, but after analysis also backwards analysis is possible
 Transition relations are code inside symbolic elements (commandfield and links between elements).
Some links:
 http://www.aseconferences.org/ase/past/ase2002/tutorials.html
 Pistore, Roveri, ITT, Delhi: Symbolic Model Checking: http://210.40.7.188/E%27ojc/MXJC/SMV/008.htm