
UNITY
 Referenced in 185 articles
[sw13461]
 UNITYbased methodology for the construction, analysis and execution of simulation models. The methodology starts ... with a simulation model specification in the form of a set of coupled state transition ... first into a set of formal assertions, permitting formal verification of the transition systems...

SCADE
 Referenced in 20 articles
[sw00829]
 embedded software. With native integration of the formallydefined Scade language, SCADE Suite ... applications spanning requirements management, modelbased design, simulation, verification, qualifiable/certified code generation, and interoperability with...

CoMA
 Referenced in 4 articles
[sw06745]
 Java software. Based on the information obtained from code execution and model simulation, the conformance ... implementation is checked with respect to its formal specification given in terms of Abstract State ... which link the concrete implementation to its formal model, without enriching the code with behavioral ... specifications for other purposes (formal verification, simulation, modelbased testing...

CD++
 Referenced in 8 articles
[sw00112]
 toolkit for modeling and simulation based on the DEVS formalism are presented. The tool ... models and easing their verification. The use of this formal approach has allowed the development ... safe and costeffective simulations, significantly reducing development time...

kPWorkbench
 Referenced in 3 articles
[sw19654]
 simulation and formal verification of kP system models using several simulation and verification methodologies ... framework features a native simulator, kPWorkbench Simulator, allowing the simulation of kP system models ... FLAME simulator, a general purpose large scale agent based simulation environment, based on a method ... model checking environment permits the formal verification of kernel P system models. The framework supports...

VATA
 Referenced in 7 articles
[sw09917]
 tree automata library applicable, e.g., in formal verification. The library supports both explicit and semi ... highly optimised reduction algorithms based on downward and upward simulations as well as algorithms...

HASL
 Referenced in 6 articles
[sw13330]
 HASL), a new temporal logic formalism for the verification of discrete event stochastic processes (DESP ... moments of path random variables. A simulationbased statistical engine is employed to obtain...

MTBDD
 Referenced in 5 articles
[sw12873]
 tree automata library applicable, e.g., in formal verification. The library supports both explicit and semi ... highly optimised reduction algorithms based on downward and upward simulations as well as algorithms...

StocHy
 Referenced in 5 articles
[sw36937]
 Abstractions are then employed for (ii) formal verification or (iii) control (policy, strategy) synthesis. StocHy ... modular modelling, and has separate simulation, verification and synthesis engines, which are implemented as independent ... implemented in C++ and employs manipulations based on vector calculus, the use of sparse matrices...

PSync
 Referenced in 5 articles
[sw17450]
 introduce PSync, a domain specific language based on the HeardOf model, which views asynchronous ... synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages ... tolerant distributed algorithms and enables automated formal verification. We have implemented an embedding of PSync...

MATF
 Referenced in 1 article
[sw41253]
 work, we propose a scheme that is based on the multiattribute trust criteria ... node identification and isolation, (b) formal modeling and verification of our proposed MATF using HLPN ... Solver, and (c) simulationbased validation and evaluation of the proposed trust framework...

SL2SX
 Referenced in 1 article
[sw20160]
 used in industry for modelbased design. Numerical simulation scales well and can be applied ... formal verification techniques to Simulink models could help to overcome this limitation. Setbased verification...

ASDeX
 Referenced in 1 article
[sw38044]
 ASDeX: a formal specification for analog circuit enabling a full automated design validation. In this ... paper an XML based language format to describe specifications of analog IPs and its usage ... based on simulation. The intention is to generate executable modules (tasks) for running simulations ... generation is based on a generic template approach using a MetaSimulator to achieve vendor...

Hybrid Trace Verifier
 Referenced in 2 articles
[sw20335]
 dynamics obtained from the formal model. Verification results from three case studies, namely, a version ... system suggest that this combined formal analysis and simulation based approach may scale to larger...

LOEWE
 Referenced in 2 articles
[sw29143]
 communication software. Although primarily based on the formal description technique LOTOS, LOEWE additionally offers multiple ... specific tool functionality: processes are used for simulation and compilation, fast state space exploration ... labelled transition graphs are used for system verification. LOEWE currently contains a LOTOS syntax...

SANDLog
 Referenced in 2 articles
[sw13794]
 been done to understand and verify the formal security guarantees of proposed secure interdomain ... step towards automated verification, we implement a verification condition generator (VCGen) to automatically extract proof ... generate executable protocol implementations; and thus, both verification and empirical evaluation of secure routing protocols ... discharging the generated verification conditions in Coq, and generated executable code based on SANDLog specification...

VCGen
 Referenced in 2 articles
[sw13795]
 been done to understand and verify the formal security guarantees of proposed secure interdomain ... step towards automated verification, we implement a verification condition generator (VCGen) to automatically extract proof ... generate executable protocol implementations; and thus, both verification and empirical evaluation of secure routing protocols ... discharging the generated verification conditions in Coq, and generated executable code based on SANDLog specification...

VeriSIMPL
 Referenced in 4 articles
[sw14598]
 opensource software for the verification of maxpluslinear systems. This work presents ... transition system are then set up based on the underlying dynamical transitions between the corresponding ... establish formal equivalences, the obtained finite abstractions are proven either to simulate or to bisimulate...

Z2sal
 Referenced in 6 articles
[sw07087]
 Z2sal: a translationbased model checker for z. Complex computer systems are difficult to implement ... correctly. To aid in the process, formal methods use mathematics in the specification ... Notation, a widelyused formal specification language. Z has been very successful in academia ... verification of systems specified as statetransition systems. It allows different verification tools...

PVSioweb
 Referenced in 2 articles
[sw11949]
 present PVSioweb which extends the simulation component of the PVS proof system with functionalities ... barriers that prevent nonexperts in formal methods from using PVS. Designers load a picture ... then explore the behaviour of the formal user interface specification through pointandclick interactions ... used as the basis for extending other verification tools. A demonstration of the capabilities...