SiLVer: Symbolic links verifier

The Core Network Algebra (CNA) is a model for concurrency that extends the point-to-point communication discipline of Milner’s CCS with multiparty interactions. Links are used to build chains describing how information flows among the different agents participating in a multiparty interaction.

SiLVer is a tool written in Maude for the animation and verification of CNA processes. Currently, the tool allows for:

• Defining processes and processes definitions.
• Generating traces from a given process.
• Building the label transition system generated from a process (in the case of finite processes)
• Generating a DOT file with the transition system of a process.
• Specifying properties of the system using Symbolic Link Modal Logic (SLML) and verify them using a model checking algorithm.
• Checking whether 2 processes are network-bisimilar.

A web interface os SiLVer is also available here.

Details on the (symbolic) verification techniques for CNA processes can be found in: Linda Brodo, Carlos Olarte: Symbolic Semantics for Multiparty Interactions in the Link-Calculus. SOFSEM 2017: LNCS (10139), pages 62-75. Springer 2017.

Code ⇦ Subtitle
The specification in Maude as well as the PHP files for the web interface are available at SiLVer site. The web interface was inspired on the CAAL project.

Authors ⇦ Subtitle
Web interface: Glauber Carvalho.
Carlos Olarte.

Contact ⇦ Subtitle
Carlos Olarte

Process definitions should start with capital letters and channel names with small letters.

CNA Expression	Syntax
Nil Process	0
Definition	A = P
Link prefix	a \ b . P
Guarded Choice	a \ b . P + c \ d . Q
Parallel Composition	P | Q
Restriction	[a , b ] P
Recursion	{ A }
Comment	# line of comments