Verfahren und System zur Durchführung einer Abstraktion einer Äusserer Schleife zur Effizienten Verifizierung Reaktiver Systeme

Details

Veröffentlichungs-Nr.

EP4530829

Aktenzeichen

EP24197004

Anmeldetag

28. August 2024

Veröffentlichung

21. Januar 2026

Erteilung

21. Januar 2026

Rechtsraum

EP

IPC

G06F8/41

Abstract

Reactive systems commonly feature an outer infinite loop that captures environmental input and according to the inputs decides the system's response. The outer infinite loop implies that almost every reactive system contains nested loops. Existing verification techniques, such as model checking and loop abstraction methods, often struggle in terms of accuracy and efficiency in the presence of nested loops. Present disclosure provides a method and a system for performing outer loop abstraction for verification of reactive systems. The system first checks whether code in outer loop can be executed before the outer loop. Then, the system performs optimization of the outer loop. Thereafter, the system abstracts outer loop which infinitely read and process environmental input. Further, the system transforms the input code to obtain outer loop abstracted code which is then passed on to an industrial verifier for verification of the reactive system.

Anmelder

Firma

Tata Consultancy Services Limited

Land

🇮🇳 Indien

Fachgebiete