IVY workbench (Home Page)

IVYworkbench

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.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)