Evaluation of Formal IDEs for Human-Machine Interface Design and Analysis: The Case of CIRCUS and PVSio-web

Camille Fayollas; Célia Martinie; Philippe Palanque; Paolo Masci; Michael D. Harrison; José C. Campos; Saulo Rodrigues e Silva

doi:10.4204/eptcs.240.1

arXiv · 1701.08465

Evaluation of Formal IDEs for Human-Machine Interface Design and Analysis: The Case of CIRCUS and PVSio-web

Camille Fayollas·Célia Martinie·Philippe Palanque·Paolo Masci·Michael D. Harrison·José C. Campos·Saulo Rodrigues e Silva

View original source ↗Read source document ↗Export metadata ↓

Abstract

Critical human-machine interfaces are present in many systems including avionics systems and medical devices. Use error is a concern in these systems both in terms of hardware panels and input devices, and the software that drives the interfaces. Guaranteeing safe usability, in terms of buttons, knobs and displays is now a key element in the overall safety of the system. New integrated development environments (IDEs) based on formal methods technologies have been developed by the research community to support the design and analysis of high-confidence human-machine interfaces. To date, little work has focused on the comparison of these particular types of formal IDEs. This paper compares and evaluates two state-of-the-art toolkits: CIRCUS, a model-based development and analysis tool based on Petri net extensions, and PVSio-web, a prototyping toolkit based on the PVS theorem proving system.

Explore related subjects

cs.HC cs.SE

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Camille Fayollas, Célia Martinie, Philippe Palanque, Paolo Masci, Michael D. Harrison, José C. Campos, Saulo Rodrigues e Silva. 2017-01-30. Evaluation of Formal IDEs for Human-Machine Interface Design and Analysis: The Case of CIRCUS and PVSio-web. https://doi.org/10.4204/eptcs.240.1

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Are explainable AI (XAI) evaluation strategies aligned? Comparing subjective, objective, and mathematical evaluation measures using saliency maps

The evaluation of explainable AI (XAI) approaches often relies on three families of methods: subjective measures (e.g., questionnaires on trust or satisfaction), objective measures (e.g., task performance metrics), and mathematical metrics (e.g., for faithfulness). Yet, it remains unclear how these families align or diverge in practice. In a{preregistered} between-subjects study (N=166), we use three established saliency map techniques (LIME, Grad-CAM, Guided Backpropagation) as a testbed to examine this issue. We find that each family of methods leads to different conclusions: participants reported no differences in trust or satisfaction, Grad-CAM improved user performance, while mathematical metrics favored Guided Backpropagation. At the same time, mathematical metrics were only partially related to user performance, and these relationships were sometimes counterintuitive. Our findings highlight the methodological importance of comparing subjective, objective, and mathematical approaches when evaluating XAI, illustrating both tensions and aspects that are aligned. We discuss implications for XAI evaluation frameworks.

cs.HC↗

arXiv2026

Mind Your Ps and Qs: Positive Moderation Practice in the Positive Queue

Online communities rely on volunteer moderators to maintain order. Despite their key role, moderators are given a toolbox of punishments and far less support for encouraging contributions they want to see more of. We introduce the Positive Queue as a positive counterpart to Reddit's modqueue: a dedicated space for moderators to discover contributions and behaviors they want to encourage and positively reinforce. With five moderators, four with 6-14 years of experience, we use the Positive Queue to examine how moderators operationalize positive reinforcement. Moderators combined predicted community reception, observed engagement, and their own judgment; used prediction-engagement mismatches to identify overlooked content; and repurposed positive features for punitive and retrospective work. These findings surface tensions around labor, attribution, and community fit. We contribute the Positive Queue as a working system and conceptualize positive moderation as recognition infrastructure that shapes what moderators notice, whose judgment becomes visible, and how recognition reaches contributors.

cs.HC↗

arXiv2026

PILOT: Control Surfaces for Authoring Social Media Feeds

Personalized social media feeds infer preferences from behavior, leaving people little direct control over what they see. Existing controls range from post-level reactions to rules and natural language, but little is known about how people use them together or how added expressiveness changes effort. We built PILOT, a Bluesky feed-authoring system that turns in-feed actions into explicit preferences, deterministic ranking, and inspectable outcomes. A study with seven participants informed an expanded implementation, which we organized into three nested control surfaces that ten participants compared within subjects. Participants assigned controls to distinct jobs: broad controls set direction, in-post actions refined results, and filters removed content. Richer surfaces did not necessarily feel more effortful, and participants' experiences depended more on whether they could verify and repair outcomes. Our findings show that usable feed control requires not simply more controls, but orchestration across mechanisms that support expression, inspection, repair, and episodic use.

cs.HC↗