About
The IVY workbench is a model based tool for the analysis of interactive systems designs. The tool acts as a frontend to the NuSMV model checker, creating an abstraction layer where models of interactive systems can be developed and analysed.
Watch the presentation (IVY v.1)...
Downloads
- Tool
- Download here
- Models
- See HCIspec@di
Related Publications
- J. Gomes, J. Gomes, M. Arcipreste and J.C. Campos (2025) Towards a More Natural Approach to Property Specification. In Human-Computer Interaction - INTERACT 2025, volume 16110 of Lecture Notes in Computer Science, pages 509-531. Springer.
- R. Braga da Costa and J.C. Campos (2023) Prototyping with the IVY Workbench: Bridging Formal Methods and User-Centred Design. In Human-Computer Interaction - INTERACT 2023, volume 14143 of Lecture Notes in Computer Science, pages 504-513. Springer.
- J.C. Campos, C. Fayollas, M.D. Harrison, C. Martinie, P. Masci and P. Palanque (2020) Supporting the analysis of safety critical user interfaces: an exploration of three formal tools. ACM Transactions on Computer-Human Interaction, 27(5), August.
- J. Araújo, R. Couto and J.C. Campos (2019) A Generator of User Interface Prototypes for the IVY Workbench. In ICGI 2019 -- International Conference on Graphics and Interaction, pages 32-39. IEEE.
- R. Couto and J.C. Campos (2019) High assurance on Cyber-Physical Interactive Systems. In HCI Engineering 2019 - Methods and Tools for Advanced Interactive Systems and Integration of Multiple Stakeholder Viewpoints, pages 46-50.
- J.C. Campos and M.D. Harrison (2019) Formal verification of interactive computing systems: opportunities and challenges. In HCI Engineering 2019 - Methods and Tools for Advanced Interactive Systems and Integration of Multiple Stakeholder Viewpoints, volume 2503 of CEUR Workshop Proceedings, pages 69-75.
- R. Couto and J.C. Campos (2019) IVY 2 - A model-based analysis tool. In The 11th ACM SIGCHI Symposium on Engineering Interactive Computing Systems - EICS 2019, pages 5:1--5:6. ACM.
- 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:17-34, April.
- M.D. Harrison, M. Drinnan, J.C. Campos, P. Masci, L. Freitas, C. di Maria and M. Whitaker (2017) Safety analysis of software components of a dialysis machine using model checking. In Formal Aspects of Component Software, volume 10487 of Lecture Notes in Computer Science, pages 137-154. Springer.
- M.D. Harrison, P. Masci, J.C. Campos and P. Curzon (2017) Demonstrating that medical devices satisfy user related safety requirements. In Software Engineering in Healthcare (FHIES/SEHC 2014), volume 9062 of Lecture Notes in Computer Science, pages 113-128. Springer.
- P. Machado, R. Couto and J.C. Campos (2017) Um editor tabular para modelação de interfaces. In Atas do EPCGI 2017 - 24o. Encontro Português de Computação Gráfica e Interação, pages 243-244.
- M. Harrison, J.C. Campos, R. Ruksenas and P. Curzon (2016) Modelling information resources and their salience in medical device design. In Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, pages 194-203. ACM.
- 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):303-316.
- M. Harrison, J.C. Campos, P. Masci and P. Curzon (2015) Templates as heuristics for proving properties of medical devices. In 5th EAI International Conference on Wireless Mobile Communication and Healthcare - "Transforming healthcare through innovations in mobile and wireless technologies". ACM.
- J.C. Campos, P. Masci, P. Curzon and M.D. Harrison (2015) Layers, resources and property templates in the specification and analysis of two interactive systems. In Proceedings of the Workshop on Formal Methods in Human Computer Interaction (FoMHCI) 2015, pages 38-43. Universitätsbibliothek, RWTH Aachen University.
- M.D. Harrison, J.C. Campos and P. Masci (2015) Reusing models and properties in the analysis of similar interactive devices. Innovations in Systems and Software Engineering, 11(2):95-111, June.
- J.C. Campos, G. Doherty and M.D. Harrison (2014) Analysing interactive devices based on information resource constraints. International Journal of Human-Computer Studies, 72(3):284-297, March.
- M. Sousa, J.C. Campos, M. Alves and M.D. Harrison (2014) Formal Verification of Safety-Critical User Interfaces: a space system case study. In Formal Verification and Modeling in Human Machine Systems: Papers from the AAAI Spring Symposium, pages 62-67. AAAI Press.
- M.D. Harrison, P. Masci, J.C. Campos and P. Curzon (2013) Automated theorem proving for the systematic analysis of an infusion pump. Electronic Communications of the EASST, 69: Formal Methods for Interactive Systems 2011. (ISSN: 1863-2122)
- M.D. Harrison, J.C. Campos, P. Masci and N. Thomas (2012) Modelling and systematic analysis of interactive systems. In Matthew L. Bolton, Asaf Degani and Philippe Palanque, editors, Proceedings of the Workshop on Formal Methods in Human-Machine Interaction (Formal H), pages 25-28.
- J.C. Campos and M.D. Harrison (2011) Modelling and analysing the interactive behaviour of an infusion pump. Electronic Communications of the EASST, 45: Formal Methods for Interactive Systems 2011. (ISSN: 1863-2122)
- J. C. Campos and M. D. Harrison (2009) Interaction engineering using the IVY tool. In ACM Symposium on Engineering Interactive Computing Systems (EICS 2009), pages 35-44. ACM.
- J.C. Campos and M.D. Harrison (2008) Considering context and users in interactive systems analysis. In Engineering Interactive Systems, volume 4940 of Lecture Notes in Computer Science, pages 193-209. Springer-Verlag. (ISBN: 978-3-540-92697-9)
- M. Harrison and J. C. Campos (2008) Analysing Human Aspects of Safety-Critical Software. ERCIM News, 75:18, October. (Invited paper; ISSN: 0926-4981)
- M. D. Harrison, J. C. Campos and K. Loer (2008) Formal analysis of interactive systems: opportunities and weaknesses. In P. Cairns and A. Cox, editors, Research Methods in Human Computer Interaction, chapter 5, pages 88-111. Cambridge University Press.
- J. C. Campos and M. D. Harrison (2008) Systematic analysis of control panel interfaces using formal tools. In XVth International Workshop on the Design, Verification and Specification of Interactive Systems (DSV-IS 2008), number 5136 of Lecture Notes in Computer Science, pages 72-85. Springer-Verlag.
- G. J. Doherty, J. C. Campos and M. D. Harrison (2008) Resources for Situated Actions. In XVth International Workshop on the Design, Verification and Specification of Interactive Systems (DSV-IS 2008), number 5136 of Lecture Notes in Computer Science, pages 194-207. Springer-Verlag.
- M. D. Harrison, J. C. Campos, G. Doherty and K. Loer (2008) Connecting rigorous system analysis to experience centred design. In E. Law, E. Hvannberg and G. Cockton, editors, Maturing Usability: Quality in Software, Interaction and Value, Human-Computer Interaction Series, chapter 3, pages 56-74. Springer. (ISSN: 1571-5035; ISBN: 978-1-84628-940-8)
- J. C. Campos and G. J. Doherty (2006) Supporting resource-based analysis of task information needs. In S.W. Gilroy and M.D. Harrison, editors, Interactive Systems: Design, Specification and Verification, volume 3941 of Lecture Notes in Computer Science, pages 188-200. Springer-Verlag. (ISSN: 0302-9743, ISBN: 3-540-34145-5)
- J. C. Campos, M. D. Harrison and Karsten Loer (2004) Verifying user interface behaviour with model checking. In J. C. Augusto and U. Ultes-Nitsche, editors, Verification and Validation of Enterprise Information Systems (VVEIS 2004), pages 87-96. INSTICC Press. (ISBN: 972-8865-03-1)