@misc(fcom,
 author       = {SAS Airbus},
 year         = {2016},
 title        = {{Airbus A380 Flight Crew Operating Manual}},
 note         = {\url{http://www.airbus.com/}},
)
@misc(a661,
 author       = {{Airlines Electronic Engineering Committee}},
 year         = {2002},
 title        = {{ARINC 661 specification: Cockpit Display System Interfaces To User Systems}},
 howpublished = {Aeronautical Radio {Inc}},
)
@inproceedings(barboni2010beyond,
 author       = {Eric Barboni and Jean-Fran\c{c}ois Ladry and David Navarre and Philippe Palanque and Marco Winckler},
 year         = {2010},
 title        = {Beyond Modelling: An Integrated Environment Supporting Co-execution of Tasks and Systems Models},
 booktitle    = {Proceedings of the 2Nd ACM SIGCHI Symposium on Engineering Interactive Computing Systems},
 series       = {EICS '10},
 publisher    = {ACM},
 pages        = {165--174},
 doi          = {10.1145/1822018.1822043},
)
@inproceedings(PIM,
 author       = {Judy Bowen and Steve Reeves},
 year         = {2013},
 title        = {Modelling Safety Properties of Interactive Medical Systems},
 booktitle    = {Proceedings of the 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems},
 series       = {EICS '13},
 publisher    = {ACM},
 pages        = {91--100},
 doi          = {10.1145/2494603.2480314},
)
@inproceedings(eics2016,
 author       = {Jos{\'e}~C. Campos and Camille Fayollas and C{\'e}lia Martinie and David Navarre and Philippe Palanque and Miguel Pinto},
 year         = {2016},
 title        = {Systematic Automation of Scenario-based Testing of User Interfaces},
 booktitle    = {Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems},
 series       = {EICS '16},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {138--148},
 doi          = {10.1145/2933242.2948735},
)
@article(MAL,
 author       = {Jos{\'e}~C. Campos and Michael~D. Harrison},
 year         = {2001},
 title        = {Model Checking Interactor Specifications},
 journal      = {Automated Software Engineering.},
 volume       = {8},
 number       = {3-4},
 pages        = {275--310},
 doi          = {10.1023/A:1011265604021},
)
@inproceedings(ivy,
 author       = {Jos{\'e}~C. Campos and Michael~D. Harrison},
 year         = {2009},
 title        = {Interaction Engineering Using the IVY Tool},
 booktitle    = {Proceedings of the 1st ACM SIGCHI Symposium on Engineering Interactive Computing Systems},
 series       = {EICS '09},
 publisher    = {ACM},
 pages        = {35--44},
 doi          = {10.1145/1570433.1570442},
)
@incollection(fomhci2016,
 author       = {Camille Fayollas and C{\'e}lia Martinie and Philippe Palanque and Eric Barboni and Racim Fahssi and Arnaud Hamon},
 year         = {In Press, 2016},
 title        = {Exploiting Action Theory as a Framework for Analysis and Design of Formal Methods Approaches: Application to the CIRCUS Integrated Development Environment},
 booktitle    = {Formal Methods in Human Computer Interaction},
 publisher    = {Springer},
)
@inproceedings(edcc2014,
 author       = {Camille Fayollas and C{\'e}lia Martinie and Philippe Palanque and Yannick Deleris and Jean-Charles Fabre and David Navarre},
 year         = {2014},
 title        = {An Approach for Assessing the Impact of Dependability on Usability: Application to Interactive Cockpits},
 booktitle    = {Proceedings of the 2014 Tenth European Dependable Computing Conference},
 series       = {EDCC '14},
 publisher    = {IEEE Computer Society},
 pages        = {198--209},
 doi          = {10.1109/EDCC.2014.17},
)
@incollection(hcse2014,
 author       = {Peter Forbrig and C{\'e}lia Martinie and Philippe Palanque and Marco Winckler and Racim Fahssi},
 year         = {2014},
 title        = {Rapid Task-Models Development Using Sub-models, Sub-routines and Generic Components},
 booktitle    = {Human-Centered Software Engineering: 5th IFIP WG 13.2 International Conference, HCSE 2014, Paderborn, Germany, September 16-18, 2014. Proceedings},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {144--163},
 doi          = {10.1007/978-3-662-44811-3_9},
)
@techreport(harrison2016,
 author       = {Michael~D. Harrison and Jos{\'e}~C. Campos and Paolo Masci},
 year         = {2016},
 title        = {{Patterns and templates for automated verification of user interface software design in PVS}},
 type         = {Technical Report},
 institution  = {{Newcastle University}},
 url          = {http://www.ncl.ac.uk/computing/research/publication/225438},
)
@incollection(HarrisonMC:16,
 author       = {Michael~D. Harrison and Paolo Masci and Jos\'e~C. Campos and Paul Curzon},
 year         = {In Press, 2016},
 title        = {The specification and analysis of use properties of a nuclear control system},
 booktitle    = {Formal Methods in Human Computer Interaction},
 publisher    = {Springer},
)
@inproceedings(heitmeyer1998scr,
 author       = {Constance Heitmeyer and James Kirby and Bruce Labaw and Ramesh Bharadwaj},
 year         = {1998},
 title        = {SCR: A toolset for specifying and analyzing software requirements},
 editor       = {Alan~J. Hu and Moshe~Y. Vardi},
 booktitle    = {Computer Aided Verification: 10th International Conference, CAV'98},
 volume       = {1427},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {526--531},
 doi          = {10.1007/BFb0028775},
)
@book(horrocks1999constructing,
 author       = {Ian Horrocks},
 year         = {1999},
 title        = {Constructing the User Interface with Statecharts},
 publisher    = {Addison-Wesley Longman Publishing Co., Inc.},
 address      = {Boston, MA, USA},
)
@article(krasner1988description,
 author       = {Glenn~E. Krasner and Stephen~T. Pope},
 year         = {1988},
 title        = {A Cookbook for Using the Model-view Controller User Interface Paradigm in Smalltalk-80},
 journal      = {Journal of Object Oriented Programming},
 volume       = {1},
 number       = {3},
 pages        = {26--49},
 url          = {http://dl.acm.org/citation.cfm?id=50757.50759},
)
@inproceedings(smc2011,
 author       = {C{\'e}lia Martinie and Philippe Palanque and Eric Barboni and Martina Ragosta},
 year         = {2011},
 title        = {Task-model based assessment of automation levels: application to space ground segments},
 booktitle    = {Systems, Man, and Cybernetics (SMC), 2011 IEEE International Conference on},
 organization = {IEEE},
 pages        = {3267--3273},
 doi          = {10.1109/ICSMC.2011.6084173},
)
@incollection(martinie2011structuring,
 author       = {C{\'e}lia Martinie and Philippe Palanque and Marco Winckler},
 year         = {2011},
 title        = {Structuring and Composition Mechanisms to Address Scalability Issues in Task Models},
 booktitle    = {Human-Computer Interaction -- INTERACT 2011: 13th IFIP TC 13 International Conference, 2011, Proceedings, Part III},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {589--609},
 doi          = {10.1007/978-3-642-23765-2_40},
)
@inproceedings(vdm,
 author       = {Paolo Masci and Peter~G. Larsen and Paul Curzon},
 year         = {2015},
 title        = {{Integrating the PVSio-web modelling and prototyping environment with Overture}},
 booktitle    = {13th Overture Workshop, satellite event of FM2015},
 publisher    = {Grace Technical Reports, Grace-TR 2015-06},
 pages        = {33--47},
 url          = {http://grace-center.jp/wp-content/uploads/2012/05/13thOverture-Proceedings.pdf},
)
@inproceedings(cav2015,
 author       = {Paolo Masci and Patrick Oladimeji and Yi~Zhang and Paul Jones and Paul Curzon and Harold Thimbleby},
 year         = {2015},
 title        = {PVSio-web 2.0: Joining PVS to HCI},
 editor       = {Daniel Kroening and P{\u{a}}s{\u{a}}reanu, S.~Corina},
 booktitle    = {Computer Aided Verification: 27th International Conference, CAV 2015, Proceedings, Part I},
 publisher    = {Springer International Publishing},
 pages        = {470--478},
 doi          = {10.1007/978-3-319-21690-4_30},
 note         = {Tool available at \url{http://www.pvsioweb.org}},
)
@misc(simulink,
 author       = {MathWorks},
 title        = {{Mathworks Simulink}},
 note         = {\url{http://www.mathworks.com/products/simulink}},
)
@inproceedings(mauro2016,
 author       = {Gioacchino Mauro and Harold Thimbleby and Andrea Domenici and Cinzia Bernardeschi},
 year         = {2016},
 title        = {Extending a user interface prototyping tool with automatic MISRA C code generation},
 booktitle    = {3rd Workshop on Formal Integrated Development Environment (F-IDE), satellite workshop of Formal Methods 2016},
 publisher    = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
)
@misc(munoz2003rapid,
 author       = {Mu{\~n}oz, C{\'e}sar~A and Ricky Butler},
 year         = {2003},
 title        = {Rapid prototyping in {PVS}},
 url          = {http://ntrs.nasa.gov/search.jsp?R=20040046914},
 note         = {{NASA/CR-2003-212418, NIA Report No.2003-03}},
)
@article(navarre2009icos,
 author       = {David Navarre and Philippe Palanque and Jean-Francois Ladry and Eric Barboni},
 year         = {2009},
 title        = {ICOs: A Model-based User Interface Description Technique Dedicated to Interactive Systems Addressing Usability, Reliability and Scalability},
 journal      = {ACM Transactions on Computer-Human Interaction (TOCHI)},
 volume       = {16},
 number       = {4},
 pages        = {18:1--18:56},
 doi          = {10.1145/1614390.1614393},
)
@inproceedings(pvs,
 author       = {Sam Owre and John~M. Rushby and Natarajan Shankar},
 year         = {1992},
 title        = {PVS: A Prototype Verification System},
 booktitle    = {Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction},
 series       = {CADE-11},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {748--752},
 doi          = {10.1007/3-540-55602-8_217},
)
@book(peterson81,
 author       = {James~Lyle Peterson},
 year         = {1981},
 title        = {Petri Net Theory and the Modeling of Systems},
 publisher    = {Prentice Hall},
)
@article(fmis2013,
 author       = {Jos{\'e}-Luis Silva and Camille Fayollas and Arnaud Hamon and C{\'e}lia Martinie and Eric Barboni},
 year         = {2014},
 title        = {{Analysis of WIMP and Post WIMP Interactive Systems based on Formal Specification}},
 journal      = {Electronic Communications of the EASST},
 volume       = {69},
 doi          = {10.14279/tuj.eceasst.69.967},
)