Tightening the contract refinements of a system architecture

DOI10.1007/s10703-017-0312-9zbMath1392.68241OpenAlexW2782218833WikidataQ62041071 ScholiaQ62041071MaRDI QIDQ1654565

Ramiro Demasi, Stefano Tonetta, Alessandro Cimatti

Publication date: 8 August 2018

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-017-0312-9

zbMATH Keywords

temporal logicparameter synthesiscontract-based designOCRA

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical problems of computer architecture (68M07) Distributed systems (68M14)

Uses Software

• nuXmv
• OCRA

Cites Work

• Unnamed Item
• Unnamed Item
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• HRELTL: a temporal logic for hybrid systems
• Multiple Viewpoint Contract-Based Specification and Design
• Requirements Validation for Hybrid Systems
• Boolean Abstraction for Temporal Logic Satisfiability