Formal Specification of Non-functional Properties of Component-Based Software


Additional Material

This page contains additional material for my paper "Formal Specification of Non-functional Properties of Component-Based Software". In particular, you can obtain the complete specifications explained in the paper. It is probably best to start with the system specification and work your way back from there. And, please let me know if you find any mistakes in any of the specifications.

Realtime

RealTime.tla

A module introducing the special variable now which models real time.

Service

Service.tla

The service context model.

ResponseTimeConstrainedService.tla

Definition of the response time measurement.

Component

Component.tla

The component context model.

ExecTimeConstrainedComponent.tla

Definition of the execution time measurement.

CPU

CPUScheduler.tla

The CPU scheduler context model.

TimedCPUScheduler.tla

Definition of the various measurements for the CPU.

RMSScheduler.tla

An RMS-scheduled CPU.

Container

SimpleContainer.tla

A simple container specification.

System

SampleSystemSpecification.tla

A very simple system specification.





Last changed: July 22, 2004