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.tla A module introducing the special variable now which models real time.


Service.tla The service context model.
ResponseTimeConstrainedService.tla Definition of the response time measurement.


Component.tla The component context model.
ExecTimeConstrainedComponent.tla Definition of the execution time measurement.


CPUScheduler.tla The CPU scheduler context model.
TimedCPUScheduler.tla Definition of the various measurements for the CPU.
RMSScheduler.tla An RMS-scheduled CPU.


SimpleContainer.tla A simple container specification.


SampleSystemSpecification.tla A very simple system specification.