• UNITY

  • Referenced in 185 articles [sw13461]
  • UNITY-based 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 formally-defined Scade language, SCADE Suite ... applications spanning requirements management, model-based 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, model-based 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 cost-effective 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 simulation-based 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 Heard-Of 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 multi-attribute trust criteria ... node identification and isolation, (b) formal modeling and verification of our proposed MATF using HLPN ... Solver, and (c) simulation-based validation and evaluation of the proposed trust framework...
  • SL2SX

  • Referenced in 1 article [sw20160]
  • used in industry for model-based design. Numerical simulation scales well and can be applied ... formal verification techniques to Simulink models could help to overcome this limitation. Set-based 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 Meta-Simulator 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 inter-domain ... 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 inter-domain ... 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]
  • open-source software for the verification of max-plus-linear 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 translation-based 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 widely-used formal specification language. Z has been very successful in academia ... verification of systems specified as state-transition systems. It allows different verification tools...
  • PVSio-web

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