PG-CBD-CVer – Component Verification

The objective of this project is to develop techniques for the analysis of functional and non-functional properties of real-time embedded systems designs described in the Progress component model. The ultimate goal is to develop a tool that supports analysis by techniques based on model-checking of the Progress component model. Three activates needed to reach this goal: a formal semantics of the Progress component model; an analysis techniques based on model-checking tailored for component models with timing; and a tool for model-checking properties of the component model. In addition, the developed technique and tool will be applied in an industrial evaluation.