short-paper

IVY 2: a model-based analysis tool

Authors:

José Creissac CamposAuthors Info & Claims

EICS '19: Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems

Article No.: 5, Pages 1 - 6

https://doi.org/10.1145/3319499.3328228

Published: 18 June 2019 Publication History

Abstract

The IVY workbench is a model-based tool that supports the formal verification of interactive computing systems. It adopts a plugin-based architecture to support a flexible development model. Over the years the chosen architectural solution revealed a number of limitations, resulting both from technological deprecation of some of the adopted solutions and a better understanding of the verification process to support. This paper presents the redesign and implementation of the original plugin infrastructure, originating a new version of the tool: IVY 2. It describes the limitations of the original solutions and the new architecture, which resorts to the Java module system in order to solve them.

References

[1]

OSGi Alliance. 2003. Osgi service platform, release 3. IOS press.

Digital Library

[2]

F. Buschmann, R. Meunier, H. Rohnert, P. Sommerlad, and M. Stal. 1996. Pattern-Oriented Software Architecture - Volume 1: A System of Patterns. Wiley.

Digital Library

[3]

J.C. Campos, M. Sousa, M. Alves, and M.D. Harrison. 2016. Formal Verification of a Space System's User Interface with the IVY workbench. IEEE Transactions on Human-Machine Systems 46, 2 (2016), 303--316.

[4]

J. C. Campos and M. D. Harrison. 2008. Systematic analysis of control panel interfaces using formal tools. In International Workshop on Design, Specification, and Verification of Interactive Systems. Springer, 72--85.

Digital Library

[5]

R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta. 2014. The nuXmv symbolic model checker. In International Conference on Computer Aided Verification. Springer, 334--342.

Digital Library

[6]

A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. 2002. NuSMV 2: An opensource tool for symbolic model checking. In International Conference on Computer Aided Verification. Springer, 359--364.

Digital Library

[7]

J. Clarke, J. Connors, and E. J. Bruno. 2009. JavaFX: Developing Rich Internet Applications. Pearson Education.

Digital Library

[8]

R. Eckstein, M. Loy, and D. Wood. 1998. Java Swing. O'Reilly & Associates, Inc.

Digital Library

[9]

C. Fayollas, C. Martinie, P. Palanque, Y. Deleris, J.-C. Fabre, and D. Navarre. 2014. An approach for assessing the impact of dependability on usability: application to interactive cockpits. In Tenth European Dependable Computing Conference. IEEE, 198--209.

Digital Library

[10]

C. Fayollas, C. Martinie, P. Palanque, P. Masci, M.D. Harrison, J.C. Campos, and S. R. Silva. 2017. Evaluation of formal IDEs for human-machine interface design and analysis: the case of CIRCUS and PVSio-web. In Third Workshop on Formal Integrated Development Environment (Electronic Proceedings in Theoretical Computer Science), Vol. 240. 1--19.

[11]

M. Feary. 2010. A Toolset for Supporting Iterative Human Automation: Interaction in Design. In Selected Papers Presented at MODSIM World 2009 Conference and Expo. NASA, 169--174.

[12]

M.D. Harrison, L. Freitas, M. Drinnan, J.C. Campos, P. Masci, C. di Maria, and M. Whitaker. 2019. Formal Techniques in the Safety Analysis of Software Components of a new Dialysis Machine. Science of Computer Programming 175 (April 2019), 17--34.

[13]

P. Masci, P. Oladimeji, Y. Zhang, P. Jones, P. Curzon, and H. Thimbleby. 2015. PVSio-web 2.0: Joining PVS to HCI. In Computer Aided Verification: 27th International Conference, CAV2015, Part I. Springer, 470--478.

[14]

F. Mazzanti and A. Ferrari. 2018. Ten Diverse Formal Models for a CBTC Automatic Train Supervision System. In Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation (Electronic Proceedings in Theoretical Computer Science), Vol. 268. 104--149.

[15]

M. Ryan, J. Fiadeiro, and T. Maibaum. 1991. Sharing Actions and Attributes in Modal Action Logic. In Theoretical Aspects of Computer Software. Lecture Notes in Computer Science, Vol. 526. Springer, 569--593.

Digital Library

[16]

R. Strniša, P. Sewell, and Ma. Parkinson. 2007. The Java module system: core design and semantic definition. ACM SIGPLAN Notices 42, 10 (2007), 499--514.

Digital Library

Cited By

Ge NWang YWang YWang YKühn TSousa V(2022)Towards the practical adoption of LIDLProceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings10.1145/3550356.3559085(12-16)Online publication date: 23-Oct-2022
https://dl.acm.org/doi/10.1145/3550356.3559085
Turner JBowen JReeves SWinckler M(2020)SeqCheckCompanion Proceedings of the 12th ACM SIGCHI Symposium on Engineering Interactive Computing Systems10.1145/3393672.3398639(1-6)Online publication date: 23-Jun-2020
https://dl.acm.org/doi/10.1145/3393672.3398639
Harrison M(2020)Examples of the Application of Formal Methods to Interactive SystemsFormal Methods. FM 2019 International Workshops10.1007/978-3-030-54994-7_31(409-423)Online publication date: 13-Aug-2020
https://doi.org/10.1007/978-3-030-54994-7_31

Index Terms

IVY 2: a model-based analysis tool
1. Human-centered computing
  1. Human computer interaction (HCI)
    1. HCI design and evaluation methods
      1. User models
  2. Interaction design
    1. Interaction design theory, concepts and paradigms
2. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
    2. Software system structures
      1. Software architectures
        Layered systems
        Publish-subscribe / event-based architectures

Recommendations

Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Kripke modelling and verification of temporal specifications of a multiple UAV system

A verifiable multiple UAV system cooperatively monitoring a road network is presented in this paper. The focus is on formal modelling and verification which can guarantee correctness of concurrent reactive systems such as multi-UAV systems. Kripke ...
Compositional reachability analysis for efficient modular verification of asynchronous designs

Compositional verification is essential to address state explosion in model checking. Traditionally, an over-approximate context is needed for each individual component in a system for sound verification. This may cause state explosion for the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

EICS '19: Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems

June 2019

141 pages

ISBN:9781450367455

DOI:10.1145/3319499

Copyright © 2019 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGCHI: ACM Special Interest Group on Computer-Human Interaction

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 June 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Short-paper

Conference

EICS '19

Sponsor:

SIGCHI

EICS '19: ACM SIGCHI Symposium on Engineering Interactive Computing Systems

June 18 - 21, 2019

Valencia, Spain

Acceptance Rates

Overall Acceptance Rate 73 of 299 submissions, 24%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
101
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)2

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ge NWang YWang YWang YKühn TSousa V(2022)Towards the practical adoption of LIDLProceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings10.1145/3550356.3559085(12-16)Online publication date: 23-Oct-2022
https://dl.acm.org/doi/10.1145/3550356.3559085
Turner JBowen JReeves SWinckler M(2020)SeqCheckCompanion Proceedings of the 12th ACM SIGCHI Symposium on Engineering Interactive Computing Systems10.1145/3393672.3398639(1-6)Online publication date: 23-Jun-2020
https://dl.acm.org/doi/10.1145/3393672.3398639
Harrison M(2020)Examples of the Application of Formal Methods to Interactive SystemsFormal Methods. FM 2019 International Workshops10.1007/978-3-030-54994-7_31(409-423)Online publication date: 13-Aug-2020
https://doi.org/10.1007/978-3-030-54994-7_31

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents