description.html - gerrit/efm - Git at Google

 <!DOCTYPE html>
 <html>
 <head>
   <link rel="stylesheet" href="styles.css">
   <title>Eclipse Formal modeling Project (EFM) - Symbex</title>
 </head>
 <body>

 	<font size=6> Eclipse Formal modeling Project (EFM) - Symbex </font>

 	<br></br>
 	<br></br>

 	Eclipse Formal modeling Project is a project dedicated to the development of model-based formal analyses. The first contribution to EFM project is Symbex, which is an extensible tool for the development of formal analysis modules (FAM in short) based on symbolic execution techniques. Symbex is part of the open source development in CEA's tool DIVERSITY. First available modules are in Symbex are dedicated to Model-based Testing including coverage heuristics. These modules are part of the open source development of. Symbex provides an expressive entry language xLIA (eXecutable Language for Interaction and Assemblage) that captures a wide range of classical models semantics (state-based models, communicating processes, UML models...). Besides, Symbex comes with a collection of Eclipse plug-ins which allows the FAM configuration and offers models editing facilities. The results of the analysis can be exported in variant of forms (symbolic tree, traces in specific formats including TTCN-3...).

 	<br></br>

 	<img src="images/efm-architecture.png" alt="tool architecture" class="center"  width="75%" height="75%" >

 				<center>Symbex's architecture </center>

 	<br></br>

 	We briefly overview some available FAMs in Symbex.

 	<ol>
 	<li> Behavior selection: This FAM is a kind of a reachability heuristic, which computes a set of symbolic states targets of some symbolic paths satisfying a coverage goal such as covering (successively) some transitions, states, I/O actions, or satisfying logical formulas on the model state variables. Such behaviors can serve as test purposes in a Model-based Testing process.</li>

 	<li> Transition coverage: This FAM explores the model with the objective is to cover at least once any transition of the model.</li>

 	<li> Symbolic state-Inclusion: This FAM stops the symbolic execution when any redundant symbolic state is included in another already-computed one in the symbolic tree: this means that the set of concrete states represented by the current symbolic state is a subset of those represented by the already-computed ones. This FAM is kind of a stopping criterion, which reduces the number of model behaviors to be considered by the analysis.</li>

 	<li> Conformity testing: This FAM implements an offline test oracle which analyzes executions of a System Under Test (SUT in short) with respected to intended behaviors specifies by the model. It analyzes timed sequence of I/O concrete actions and waiting delays to deliver a test verdict (Pass, Fail, Inconc ...).</li>
 	</ol>


 	<img src="images/efm-screen.png" alt="tool architecture" width="80%" height="80%" class="center">

 						<center>Screenshot of Symbex's Eclipse GUI </center>

 </body>

 </html>
	<!DOCTYPE html>
	<html>
	<head>
	<link rel="stylesheet" href="styles.css">
	<title>Eclipse Formal modeling Project (EFM) - Symbex</title>
	</head>
	<body>

	<font size=6> Eclipse Formal modeling Project (EFM) - Symbex </font>

	<br></br>
	<br></br>

	Eclipse Formal modeling Project is a project dedicated to the development of model-based formal analyses. The first contribution to EFM project is Symbex, which is an extensible tool for the development of formal analysis modules (FAM in short) based on symbolic execution techniques. Symbex is part of the open source development in CEA's tool DIVERSITY. First available modules are in Symbex are dedicated to Model-based Testing including coverage heuristics. These modules are part of the open source development of. Symbex provides an expressive entry language xLIA (eXecutable Language for Interaction and Assemblage) that captures a wide range of classical models semantics (state-based models, communicating processes, UML models...). Besides, Symbex comes with a collection of Eclipse plug-ins which allows the FAM configuration and offers models editing facilities. The results of the analysis can be exported in variant of forms (symbolic tree, traces in specific formats including TTCN-3...).

	<br></br>

	<img src="images/efm-architecture.png" alt="tool architecture" class="center" width="75%" height="75%" >

	<center>Symbex's architecture </center>

	<br></br>

	We briefly overview some available FAMs in Symbex.

	<ol>
	<li> Behavior selection: This FAM is a kind of a reachability heuristic, which computes a set of symbolic states targets of some symbolic paths satisfying a coverage goal such as covering (successively) some transitions, states, I/O actions, or satisfying logical formulas on the model state variables. Such behaviors can serve as test purposes in a Model-based Testing process.</li>

	<li> Transition coverage: This FAM explores the model with the objective is to cover at least once any transition of the model.</li>

	<li> Symbolic state-Inclusion: This FAM stops the symbolic execution when any redundant symbolic state is included in another already-computed one in the symbolic tree: this means that the set of concrete states represented by the current symbolic state is a subset of those represented by the already-computed ones. This FAM is kind of a stopping criterion, which reduces the number of model behaviors to be considered by the analysis.</li>

	<li> Conformity testing: This FAM implements an offline test oracle which analyzes executions of a System Under Test (SUT in short) with respected to intended behaviors specifies by the model. It analyzes timed sequence of I/O concrete actions and waiting delays to deliver a test verdict (Pass, Fail, Inconc ...).</li>
	</ol>


	<img src="images/efm-screen.png" alt="tool architecture" width="80%" height="80%" class="center">

	<center>Screenshot of Symbex's Eclipse GUI </center>

	</body>

	</html>