FACTum Studio

Contents

Overview
Installation Instructions
Publish-subscribe Pattern Tutorial

Overview

FACTum Studio is a tool that supports Architectural Design Patterns (ADPs) specification and verification with the support of interactive verification in Isabelle/HOL.

At this stage of development, the tool has the following key features mainly for specification of ADPs:

The tool is developed using the Eclipse Modeling Framework (EMF), particularly, with Obeo’s free and ready-to-use Eclipse package Obeo Designer Community. It includes the technologies required for the development, such as Sirius, Xtext, and Xtend.

Installation Instructions

A working copy of Obeo Designer Community edition should enable the importing of the FACTum tool metamodel project and runtime sample to start and try the tool. Currently, FACTum Studio works with Obeo Designer Community Version 10.1. Other versions may not run as expected. You may download files required from the following links:

Publish-subscribe Pattern Tutorial

The video tutorial below shows a brief overview of using FACTum Studio. The tutorial demonstrates the tool with a specification of the publish-subscribe pattern and transforms the specification to Isabelle/HOL for verification.

Publish-subscribe pattern tutorial