E-FMP's Extensible Symbolic Execution Tool
0EclipseCon France 2018
https://www.eclipsecon.org/france2018/session/e-fmps-extensible-symbolic-execution-tool
Speaker(s):
Mathilde Arnaud (CEA)
Eclipse Formal Modeling Project -E-FMP for short- provides an extensible tool called SymbEx for the development of model-based formal analyses using symbolic execution. This is the first tool to be contributed to the E-FMP project. SymbEx comes with an expressive entry language that captures a wide range of classical models semantics: e.g., UML/SysML, SDL, (Timed) Symbolic Transition Systems and abstractions of Hybrid Automata... SymbEx provides developers with extension mechanisms allowing customizing the basic symbolic treatments to implement specific Formal Analysis Modules -FAM for short- (e.g., Model-based Testing -MBT for short- algorithms, exploration strategies and heuristics...). SymbEx is connected with SMT solvers, e.g., CVC4, Z3 and YICES which can be easily used to implement new FAMs. In fact, SymbEx provides "hooks" into the basic well-known symbolic execution algorithm which allow FAMs -by implementing specific pre-process or post-process or pre-filter or post-filter methods to customize symbolic treatments at different steps of the execution. We present these extensions facilities offered by the SymbEx tool. We also discuss how to use those facilities to develop some FAMs which implement reachability-based formal analyses up to coverage criteria.