Thorium: A Language for Bounded Verification of Dynamic Reactive Objects

Simple item page
dc.contributor.authorBaldor, Kevin
dc.contributor.authorWang, Xiaoyin
dc.contributor.authorNiu, Jianwei
dc.date.accessioned2023-12-04T16:22:31Z
dc.date.available2023-12-04T16:22:31Z
dc.date.issued2023-10-19
dc.description.abstractDeveloping reliable reactive software is notoriously difficult – particularly when that software reacts by changing its behavior. Some of this difficulty is inherent; software that must respond to external events as they arrive tends to end up in states that are dependent on the value of that input and its order of arrival. This results in complicated corner cases that can be challenging to recognize. However, we find that some of the complexity is an accident of the features of the programming languages widely used in industry. The loops and subroutines of structured programming are well-suited to data transformation, but poorly capture – and sometimes obscure – the flow of data through reactive programs developed using the inversion-of-control paradigm; an event handler that modifies the data flow tends to be declared closer to the definition of the event that activates it than to the initial definition of the data flow that it modifies. This paper approaches both challenges with a language inspired by the declarative modules of languages SIGNAL and Lustre and the semantics of the SodiumFRP Functional Reactive Programming library with a declarative mechanism for self modification through module substitution. These language features lead to software with a code structure that closely matches the flow of data through the running program and thus makes software easier to understand. Further, we demonstrate how those language features enable a bounded model checking approach that can verify that a reactor meets its requirements or present a counterexample trace, a series of states and inputs that lead to a violation. We analyze the runtime performance of the verifier as a function of model size and trace length.
dc.description.departmentComputer Science
dc.identifier.citationBaldor, K., Wang, X., & Niu, J. (2023). Thorium: A Language for Bounded Verification of Dynamic Reactive Objects. Paper presented at the 10th ACM SIGPLAN International Workshop on Reactive and Event-Based Languages and Systems, Cascais, Portugal. https://doi.org/10.1145/3623506.3623574
dc.identifier.isbn979-8-4007-0400-0
dc.identifier.otherhttps://doi.org/10.1145/3623506.3623574
dc.identifier.urihttps://hdl.handle.net/20.500.12588/2265
dc.language.isoen
dc.publisherAssociation for Computing Machinery
dc.rightsAttribution 3.0 United Statesen
dc.rights.urihttp://creativecommons.org/licenses/by/3.0/us/
dc.subjectbounded model checking
dc.subjectfunctional reactive programming
dc.titleThorium: A Language for Bounded Verification of Dynamic Reactive Objects
dc.typeArticle

Files

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
Name:
Baldor et al 2023 - Thorium- A Language for Bounded Verification of Dynamic Reactive Objects.pdf
Size:
249.62 KB
Format:
Adobe Portable Document Format
Download

License bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.86 KB
Format:
Item-specific license agreed upon to submission
Description:
Download

Collections

College of Sciences Faculty Research