En ram för att framkalla och avlusa formella specifikationer för cyberfysiska system presenteras. Framkallandet av specifikationer hanteras genom ett grafiskt gränssnitt. Två felsökningsalgoritmer presenteras. De första kontrollerna av felaktiga eller ofullständiga tidslogiska specifikationer utan att ta hänsyn till systemet. Den andra kan användas för analys av reaktiva krav med avseende på systemtestspår. Specifikationens felsökningsram tillämpas på ett antal formella specifikationer som samlas in genom en användarstudie. I användarstudien fastställs att kravfel är vanliga och att felsökningsramen kan lösa många försåtliga specifikationsfel. A. Dokhanchi m.fl. (1) Giltighetsdetektering: specifikationen är otillfredsställande eller en tautologi. (2) Detektion av redundans: formeln har redundanta konjunkturer. (3) Detektion av vakuitet: Vissa underformer påverkar inte tillfredsställandet av formeln. Löslighets- och vakuumfrågor tyder vanligtvis på ett visst missförstånd i fråga om kraven. Som ett resultat av detta kan en bred klass av specifikationsfel i framkallningsprocessen korrigeras innan någon test- och verifieringsprocess inleds. Vissa specifikationsproblem kan dock inte upptäckas om vi inte tar hänsyn till systemet och testar systemets beteende med avseende på specifikationen. Vi tillhandahåller algoritmer för att upptäcka specifikationsvakuum med avseende på systemspår för att hjälpa 1 Den anonyma online-enkäten finns tillgänglig via: http://goo.gl/forms/YW0reiDtgi.
I REF föreslås en ram för framtagande och felsökning av formella specifikationer för cyberfysiska system genom två felsökningsalgoritmer.
Formal Requirement Debugging for Testing and Verification of Cyber-Physical Systems
{'venue': 'TECS', 'journal': None, 'mag_field_of_study': ['Mathematics', 'Computer Science']}