Deriving real-time monitors from system requirements documentation
Bibliographic record
Abstract
During system testing, determining if the observed behaviour of a real–time system is consistent with its requirements specification can be difficult. I propose that a system to check the behaviour against the specification, a monitor, be automatically derived from the requirements documentation. The monitor would model the system requirements as a modified finite state automaton in which the states represent equivalence classes of system histories and transitions are labelled with predicates such that it accepts only executions representing acceptable system behaviour. Investigation into the design of such a monitor, and the process for automatically generating it from reviewable requirements documentation is on–going. 1. Problem Statement The process of testing a real–time system typically involves running the system in a test environment, observing its behaviour and comparing it to that required by its specification. In general, making this comparison can be quite difficult since the requirements may be complex, possibly including time constraints and interdependencies. A monitor is a system that automatically determines if the observed behaviour is consistent with a given specification. When designing safety– or mission–critical systems, good engineering practice dictates that a clear, precise and unambiguous specification of the required behaviour of the system be produced and reviewed for correctness by experts in the domain of application of the system. Research has demonstrated that such reviews are effective if the system behavioural requirements documentation is written such that: it expresses the required behaviour in terms of the quantities from the environment that are monitored and/or controlled by the system, it uses terminology and notation that is familiar to, or easily understood by, the domain experts, and it is presented in a manner that permits independent review of small parts of the document.[5] As discussed in [4], [9], [12] and [13], a (relational) system requirements document describes a relation, REQ, on vector functions of time representing the environmental quantities that are monitored and controlled by the system. I intend to explore techniques for using reviewable forms of such documentation (i.e. satisfying the above three criteria) to generate a software monitor that will determine if the observed behaviour of some software is consistent with that expressed in the documentation. Such a monitor would be useful, during system testing, for determining if the system is operating correctly, or, in certain safety–critical applications, it may be useful as a redundant monitoring system during operation. Through this research I hope to answer the following questions: 1. How can a monitor be used to verify conformance with relational requirements documentation? 2. What are the useful classes of behavioural properties that can and cannot be: a) specified in relational documentation? b) verified using a monitor as described above? 3. Under what conditions can an effective monitor be produced automatically from a relational requirements document? What restrictions on the form or content of the documentation must be imposed? 4. What is the cost (computational and space complexity) of using such a monitor? Are there some optimizations that can be done to reduce this complexity or restrictions on the documentation that will ensure that the complexity is tractable?
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame machine prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. The Gemma side is a direct model label for every work in the frame, read from the title-only record. The Codex side is a classifier learned from the 10,348 direct Codex labels and calibrated to design-weighted sample rates; fields without enough sample support carry no Codex call. Candidate is the union of the two sides; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels.
Distilled classifier scores by category (both heads)
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.011 | 0.071 |
| Meta-epidemiology (narrow) | 0.001 | 0.002 |
| Meta-epidemiology (broad) | 0.001 | 0.002 |
| Bibliometrics | 0.003 | 0.001 |
| Science and technology studies | 0.001 | 0.001 |
| Scholarly communication | 0.003 | 0.003 |
| Open science | 0.002 | 0.002 |
| Research integrity | 0.002 | 0.002 |
| Insufficient payload (model declined to judge) | 0.003 | 0.002 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one source (direct Gemma or distilled Codex), not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".