Additional Material - Formal Specification of Non-functional Properties of Component-Based Software
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. |