Deriving real-time monitors from system requirements documentation
Notice bibliographique
Résumé
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?
Récupéré en direct depuis OpenAlex et désinversé. Les résumés ne sont pas conservés dans cette base de données : les index inversés représentent 8,6 Go des 9,3 Go de texte de la base, et le serveur dispose de 13 Go libres.
Comment cette classification a été obtenuedéplier
Prédiction machine sur la base complète
Imitation des enseignantsNi prévalence calibrée, ni vérité terrain. Validation humaine à venir. Le volet Gemma est une étiquette directe du modèle pour chaque travail de la base, lue sur la notice réduite au titre. Le volet Codex est un classifieur appris des 10 348 étiquettes directes de Codex et calibré sur les taux pondérés de l'échantillon; les champs sans appui suffisant ne portent aucun appel Codex. Le mode candidate est l'union des deux volets; le consensus est leur intersection. Ces sorties portent le statut machine_predicted_unvalidated et ne sont pas des étiquettes humaines.
Scores du classifieur distillé par catégorie (deux têtes)
| Catégorie | Codex | Gemma |
|---|---|---|
| Métarecherche | 0,011 | 0,071 |
| Méta-épidémiologie (sens strict) | 0,001 | 0,002 |
| Méta-épidémiologie (sens large) | 0,001 | 0,002 |
| Bibliométrie | 0,003 | 0,001 |
| Études des sciences et des technologies | 0,001 | 0,001 |
| Communication savante | 0,003 | 0,003 |
| Science ouverte | 0,002 | 0,002 |
| Intégrité de la recherche | 0,002 | 0,002 |
| Charge utile insuffisante (le modèle a refusé de juger) | 0,003 | 0,002 |
Scores machine (provisoires)
Les deux têtes enseignantes du modèle étudiant, lues sur ce travail. Un score ordonne la base pour la relecture; il n'affirme jamais une catégorie, et le statut de validation accompagne chaque rangée tel quel.
Scores de référence d'un modèle non mature (critères de maturité non atteints, 7 itérations). Un score ordonne; il n'affirme jamais une catégorie.
score_only:v0-immature-baseline · tel quel depuis la passe de notation : score_only signifie que le nombre peut ordonner les travaux, et qu'aucune étiquette de catégorie n'en découleClassification
machine, non validéePrédiction automatique; un appel candidat d’une seule source (Gemma direct ou Codex distillé), pas un consensus.
Le détail, modèle par modèle et score par score, se trouve en fin de page sous « Comment cette classification a été obtenue ».