2 citations · 4 across the 3 of their papers we have counts for
7 papers · 1 filter
Synthesis of Infinite-State Systems with Random Behavior
Andreas Katis, Grigory Fedyukovich, Jeffrey Chen +3
Diversity in the exhibited behavior of a given system is a desirable characteristic in a variety of application contexts. Synthesis of conformant implementations often proceeds by…
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts
Andreas Katis, Grigory Fedyukovich, Huajun Guo +4
Automated synthesis of reactive systems from specifications has been a topic of research for decades. Recently, a variety of approaches have been proposed to extend synthesis of re…
Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability
Andreas Katis, Grigory Fedyukovich, Andrew Gacek +3
The realizability problem in requirements engineering is to determine the existence of an implementation that meets the given formal requirements. A step forward after realizabilit…
On Implementing Real-time Specification Patterns Using Observers
John D. Backes, Michael W. Whalen, Andrew Gacek +1
English language requirements are often used to specify the behavior of complex cyber-physical systems. The process of transforming these requirements to a formal specification lan…
Towards Synthesis from Assume-Guarantee Contracts involving Infinite Theories: A Preliminary Report
Andreas Katis, Michael W. Whalen, Andrew Gacek
In previous work, we have introduced a contract-based real- izability checking algorithm for assume-guarantee contracts involving infinite theories, such as linear integer/real ari…
Requirements Analysis of a Quad-Redundant Flight Control System
John Backes, Darren Cofer, Steven Miller +1
In this paper we detail our effort to formalize and prove requirements for the Quad-redundant Flight Control System (QFCS) within NASA's Transport Class Model (TCM). We use a compo…