High-integrity Java Applications using Circus
Lead Research Organisation:
University of York
Department Name: Computer Science
Abstract
The use of computers and computer programs is pervasive nowadays, but every computer user knows that programs go wrong. While it is just annoying when our favourite text editor loses a bit of our work, the consequences are potentially much more serious when a computer program that, for instance, controls parts of an airplane goes wrong. Software validation and verification are central to the development of this sort of application. In fact, the software industry in general spends a very large amount of money in these activities. One of the measures taken to promote correctness of programs is the use of a restricted set of features available in programming languages. This usually means that most of the more recent advances in software engineering are left out. In this project, we propose to provide development, validation, and verification facilities that allow object-orientation and a modern real-time computational model to be used for the programming of safety-critical systems. In particular, we will work with one of the most popular programming languages: Java, or more specifically, its profiles for high-integrity engineering proposed by the Open Group. As our main case study, we will verify parts of the controller of the first Java Powered Industrial Robot, developed by Sun. One of our collaborators, a senior engineer in Sun tells in an interview that Distributed Real-Time Systems are really hard to build and the engineering community doesn't really know how to build them in a coherent repeatable way. (java.dzone.com/articles) Real-Time Java is entering the industrial automation and automotive markets. Lawyers did not allow the Java Robot to get anywhere near a human, even in a JavaOne conference demo. To proceed in that kind market, better support is needed.Programming is just one aspect of the development of a modern system; typically, a large number of extra artefacts are produced to guide and justify its design. Just like several models of a large building are produced before bricks and mortar are put together, several specification and design models of a program are developed and used before programs are written. These models assist in the validation and verification of the program. To take our civil engineering metaphor one step further, we observe that, just like there can be various models of a building that reflect several points of view, like electricity cabling, plumbing, and floor plans, for example, we also have several models of a system. Different modelling and design notations concentrate on different aspects of the program: data models, concurrent and reactive behaviour, timing, and so on. No single notation or technique covers all the aspects of the problem, and a combination of them needs to be employed in the development of large complex systems. In this project, we propose to investigate a novel integrated approach to validation and verification. Our aim is to provide a sound and practical technique that covers data modelling, concurrency, distribution, and timing. For that, we plan to investigate the extension and combined use of validation and verification techniques that have been successfully applied in industry. We do not seek an ad hoc combination of notations and tools, but a justified approach that provides a reliable foundation for the use of practical techniques. We will have succeeded if we verify a substantial part of the robot controller: using a model written in our notation, we will apply our techniques to verify parts of the existing implementation, execute it using our verified implementation of Safety-critical Java. Measure of success will be provided by our industrial partners and the influence of our results in their practice or business plans.
Organisations
- University of York (Lead Research Organisation)
- Southwest University (Collaboration)
- Aarhus University (Collaboration)
- Universidade de São Paulo (Collaboration)
- University Paris Sud (Collaboration)
- Newcastle University (Collaboration)
- Microsoft Research (Collaboration)
- Trinity College Dublin (Collaboration)
- Praxis Systems Ltd (Collaboration)
- BRUNEL UNIVERSITY LONDON (Collaboration)
- University of Bremen (Collaboration)
- Indian Institute of Science Bangalore (Collaboration)
- Altran (United Kingdom) (Project Partner)
- IBM (Canada) (Project Partner)
- Atomic Weapons Establishment (Project Partner)
- Sun Microsystems Ltd (Project Partner)
Publications
Zhao H
(2021)
Learning safe neural network controllers with barrier certificates
in Formal Aspects of Computing
Zeyda F
(2012)
Mechanised support for sound refinement tactics
in Formal Aspects of Computing
Zeyda F
(2013)
Unifying Theories of Programming
Zeyda F
(2013)
Refining SCJ Mission Specifications into Parallel Handler Designs
in Electronic Proceedings in Theoretical Computer Science
Zeyda F
(2012)
Mechanical reasoning about families of UTP theories
in Science of Computer Programming
Zeyda F
(2015)
Laws of mission-based programming
in Formal Aspects of Computing
Zeyda F
(2010)
Unifying Theories of Programming
Zeyda F
(2011)
Formal Methods: Foundations and Applications
Description | The use of computers and computer programs is pervasive nowadays, but every computer user knows that programs go wrong. While it is just annoying when our favourite text editor loses a bit of our work, the consequences are potentially much more serious when a computer program that, for instance, controls parts of an airplane goes wrong. Software validation and verification are central to the development of this sort of application. In fact, the software industry in general spends a very large amount of money in these activities. One of the measures taken to promote correctness of programs is the use of a restricted set of features available in programming languages. This usually means that most of the more recent advances in software engineering are left out. In this project, we have desgined techniques to support development, validation, and verification facilities that allow modern programming technology (object-orientation and an advanced real-time computational model) to be used in safety-critical systems. In particular, we have considered one of the most popular programming languages: Java and its two profiles for high-integrity engineering proposed by the Open Group, namely SCJ (Safety-Critical Java) Levels 1 and 2. We have also produced a technique to allow the verification that the extra software that needs to run in machines to enable the execution of SCJ programs is correct and in accordance with the Open Group Standard. |
Exploitation Route | Others can use our results by adopting Java as a programming language, in particular, the version for safety-critical systems. They are now in a position to consider the application of verification techniques based on mathematics (formal methods) as suggested by regulators (DO-178C), for instance. The Open Group that is responsible for the standardisation of SCJ has been benefiting of our results. We are in constant contact, and have influenced the evolution of the SCJ language in many ways. There are many ways in which the research can be taken forward. The suitability of the techniques has generated theoretical results (namely, semantic theories for time and object orientation) that are particular assets of general interest. The SCJ standardisation group has considered the possibility of combining SCJ with another programming language, called Scala, to ease validation and verification. This imposes challenges in terms of the implementation platform for SCJ, and we are discussing with colleagues the development of verified platforms of mixed criticality. We now have developed techniques to enable verification of programming platforms for SCJ. |
Sectors | Aerospace Defence and Marine Agriculture Food and Drink Digital/Communication/Information Technologies (including Software) Electronics Healthcare Transport |
URL | http://www.cs.york.ac.uk/circus/hijac/index.html |
Description | Yes, they have been used by the Open Group that is in charge of defining Safety-Critical Java. We are in close contact, and have influenced several aspects of the definition of the language. These cover core aspects of Safety-Critica Java: its schedule and memory management mechanisms. The JCP (Java Community Process) has now approved the specification (https://jcp.org/en/jsr/results?id=6271). JCP is the mechanism for developing standard technical specifications for Java technology. |
First Year Of Impact | 2021 |
Sector | Digital/Communication/Information Technologies (including Software) |
Impact Types | Cultural Economic |
Description | 1000 Talents Programme |
Amount | ¥1,950,000 (CNY) |
Organisation | National Science Foundation China |
Sector | Public |
Country | China |
Start | 11/2019 |
End | 11/2024 |
Description | Aarhus University Centre for Digital Twins |
Amount | 970,392 kr. (DKK) |
Funding ID | 2018-019 |
Organisation | Aarhus University |
Sector | Academic/University |
Country | Denmark |
Start | 11/2019 |
End | 11/2024 |
Description | EMRP |
Amount | € 100,000 (EUR) |
Funding ID | NEW06-REG4(UoY) |
Organisation | European Association of National Metrology Institutes (EURAMET) |
Sector | Charity/Non Profit |
Country | Germany |
Start | 05/2014 |
End | 05/2015 |
Description | EPSRC Standard Grant |
Amount | £1,776,973 (GBP) |
Funding ID | EP/R025479/1 |
Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
Sector | Public |
Country | United Kingdom |
Start | 03/2018 |
End | 03/2023 |
Description | EPSRC responsive mode |
Amount | £1,029,474 (GBP) |
Funding ID | EP/H017461/1 |
Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
Sector | Public |
Country | United Kingdom |
Start | 05/2010 |
End | 09/2015 |
Description | EU FP7 |
Amount | € 1,000,000 (EUR) |
Organisation | European Commission |
Sector | Public |
Country | European Union (EU) |
Start | 09/2011 |
End | 09/2014 |
Description | EU Horizon 2020 |
Amount | € 900,000 (EUR) |
Organisation | European Commission |
Sector | Public |
Country | European Union (EU) |
Start | 01/2015 |
End | 12/2017 |
Description | Horizon 2020 |
Amount | € 7,000,000 (EUR) |
Organisation | European Commission |
Sector | Public |
Country | European Union (EU) |
Start | 01/2015 |
End | 12/2017 |
Description | International Exchanges Scheme |
Amount | £9,900 (GBP) |
Organisation | The Royal Society |
Sector | Charity/Non Profit |
Country | United Kingdom |
Start | 03/2012 |
End | 03/2014 |
Description | Newton Mobility Grant |
Amount | £12,000 (GBP) |
Organisation | The Royal Society |
Sector | Charity/Non Profit |
Country | United Kingdom |
Start | 12/2015 |
End | 11/2017 |
Description | RAEng Brazil 1 |
Amount | £24,000 (GBP) |
Funding ID | NRCP1617/5/68 |
Organisation | Royal Academy of Engineering |
Sector | Charity/Non Profit |
Country | United Kingdom |
Start | 05/2016 |
End | 07/2017 |
Description | RAEng Brazil 2 |
Amount | £24,000 (GBP) |
Funding ID | NRCP1617/6/164 |
Organisation | Royal Academy of Engineering |
Sector | Charity/Non Profit |
Country | United Kingdom |
Start | 01/2017 |
End | 01/2018 |
Description | Seventh Framework Programme |
Amount | € 6,000,000 (EUR) |
Funding ID | 287829 |
Organisation | European Commission |
Sector | Public |
Country | European Union (EU) |
Start | 09/2011 |
End | 09/2014 |
Description | Aarhus University Centre for Digital Twins |
Organisation | Aarhus University |
Department | School of Engineering |
Country | Denmark |
Sector | Academic/University |
PI Contribution | Research collaboration with Professor Peter Gorm Larsen at Aarhus University's Centre for Digital Twins. Appointment as Adjunct Professor with support for activities, including regular visits. Appointment of Larsen as Visiting Professor at York. |
Collaborator Contribution | Collaboration on research papers and research proposals. Joint supervision of students at Aarhus. |
Impact | Collaboration with Cláudio Gomes on a paper: Uncertainty quantification and runtime monitoring using environment-aware digital twins. Paper accepted for ISoLA conference 2020, but delayed to 2021 because of pandemic. |
Start Year | 2019 |
Description | Adjunct Professorship, Southwest University, Chongqing, China |
Organisation | Southwest University |
Country | China |
Sector | Academic/University |
PI Contribution | Collaboration on a joint research project on human-cyber-physical systems. Appointment as Adjunct professor at Southwest University. Supervision of joint research students at Southwest University. Personal research fund for JCPW at Southwest University. Collaboration on the verification of neural networks. |
Collaborator Contribution | Joint research papers and research proposals. Proposed joint research laboratory. Joint direction of FM4AI research programme. |
Impact | Published a paper: Hengjun Zhao, Xia Zeng, Taolue Chen, Zhiming Liu, Jim Woodcock: Learning Safe Neural Network Controllers with Barrier Certificates. SETTA 2020: 177-185 |
Start Year | 2019 |
Description | Butterfield TCD UTP |
Organisation | Trinity College Dublin |
Department | School of Computer Science and Statistics |
Country | Ireland |
Sector | Academic/University |
PI Contribution | I have been collaborating with Andrew Butterfield since 2002 on Unifying Theories of Programming (UTP) and the formal semantics of of real-time, hybrid, and probabilistic systems. We meet regularly (at least twice a year) and have published 10 joint papers (five journal and five refereed conference papers). I have made contributions in foundations of UTP (including donating extensive course materials) and in applications to systems of systems and robotic and autonomous systems. |
Collaborator Contribution | Andrew Butterfield at TCD has made contributions to understanding hardware/software co-design and real-time and probabilistic systems. He contributed a strong background in functional programming. |
Impact | Outputs: DOIs: 10.1007/978-3-319-47166-2_26 10.1016/j.scico.2008.09.014 10.1109/TASE.2009.57 10.1109/ICECCS.2008.35 10.1109/ICECCS.2007.23 10.1007/978-3-540-73210-5_5 10.1016/j.entcs.2006.04.026 10.1007/s10009-004-0181-6 10.1016/S1571-0661(04)80821-1 10.1016/S1571-0661(04)80762-X The collaboration is multi-disciplinary, involving computer science and electronic engineering. |
Description | D'Souza IISc Verification |
Organisation | Indian Institute of Science Bangalore |
Department | Department of Computer Science and Automation |
Country | India |
Sector | Academic/University |
PI Contribution | My team contributed expertise in formal specification, refinement, and verification of software. We contributed to the verification of FreeRTOS, the popular open-source real-time operating system. We helped our Indian colleagues develop expertise in Z and Z/Eves and helped them apply it to verification problems. |
Collaborator Contribution | Colleagues at the Indian Institute of Science and General Motors India helped us to understand the FreeRTOS code and extract suitable abstract specifications of aspects of its behaviour. |
Impact | Three projects funded by the British Council, the Royal Academy of Engineering, and the Robert Bosch Centre for Cyber-Physical Systems (total value £175k). One conference paper (10.1007/978-3-319-25423-4_11). One journal paper (10.1007/s00165-014-0308-9). Two Phd theses: Sumesh Divakaran: A Refinement-Based Methodology for Verifying Abstract Data Type Implementations (IISc, 2015). Shu Cheng: Formally modelling and verifying the FreeRTOS real-time operating system (York, 2014). |
Start Year | 2010 |
Description | FitzLarsen CPS EU |
Organisation | Aarhus University |
Department | School of Engineering |
Country | Denmark |
Sector | Academic/University |
PI Contribution | Our collaboration has involved two major EU projects. My research team brought expertise in modelling, formal semantics, mechanised proof, and model checking. |
Collaborator Contribution | Newcastle made contribution in modelling and methods. Aarhus made contributions in tool building. |
Impact | Also see http://www.compass-research.eu/. Outputs: Funding for two large EU projects. Publications: 8 conference papers, 4 journal papers, 2 book chapters. Citations: > 600 in total. Multi-disciplinary collaboration covering systems, software, hardware, control theory, and electronics. |
Start Year | 2009 |
Description | Formal testing |
Organisation | University Paris Sud |
Country | France |
Sector | Academic/University |
PI Contribution | All the work on formal model-based testing based on the notation of relevance. |
Collaborator Contribution | This is a scientific collaboration, and we developed testing theories and techniques in collaboration. |
Impact | Joint papers |
Start Year | 2007 |
Description | Process-algebra based testing for refinement with inputs and outputs |
Organisation | Brunel University London |
Department | Department of Education |
Country | United Kingdom |
Sector | Academic/University |
PI Contribution | Expertise in process algebra and refinement, and testing for refinement based on process algebra. |
Collaborator Contribution | Testing with inputs and outputs and distributed systems. |
Impact | A. L. C. Cavalcanti, R. M. Hierons, S. Nogueira, and A. C. A. Sampaio. A suspension-trace semantics for CSP. In International Symposium on Theoretical Aspects of Software Engineering, pages 3--13, 2016. Invited paper. A. L. C. Cavalcanti, M.-C. Gaudel, and R. M. Hierons. Conformance Relations for Distributed Testing based on CSP. In B. Wolff and F. Zaidi, editors, IFIP International Conference on Testing Software and Systems, Lecture Notes in Computer Science. Springer-Verlag, 2011. A. L. C. Cavalcanti and R. M. Hierons. Testing with Inputs and Outputs in CSP. In Fundamental Approaches to Software Engineering, volume 7793 of Lecture Notes in Computer Science, pages 359-374, 2013. |
Start Year | 2011 |
Description | SCJ VM Verification |
Organisation | Newcastle University |
Country | United Kingdom |
Sector | Academic/University |
PI Contribution | We are working together on the verification of an SCJ VM. In our group, we are contributing to the development of the virtual macine. |
Collaborator Contribution | They are leading the modelling of the virtual machine and the proof that it is correct. |
Impact | L. Freitas, J. Baxter, A. L. C. Cavalcanti, and A. Wellings. Modelling and verifying a priority scheduler for an SCJ runtime environment. In Integrated Formal Methods, Lecture Notes in Computer Science. Springer, 2016. J. Baxter, A. L. C. Cavalcanti, A. J. Wellings, and L. Freitas. Safety-Critical Java Virtual Machine Services. In L. Ziarek, editor, 13th International Workshop on Java Technologies for Real-time and Embedded Systems, pages 7:1--7:10. ACM, 2015. |
Start Year | 2014 |
Description | Testing from Circus with Mealy Machines |
Organisation | Universidade de São Paulo |
Department | Institute of Mathematical and Computer Sciences (ICMC) |
Country | Brazil |
Sector | Academic/University |
PI Contribution | Expertise on model-based testing based on process algebras and resfinement. |
Collaborator Contribution | Expertise on testing based on Mealy machines. |
Impact | Joint papers |
Start Year | 2015 |
Description | VSR collaborations |
Organisation | Microsoft Research |
Department | Microsoft Research Cambridge |
Country | United Kingdom |
Sector | Private |
PI Contribution | Organising the UK's contribution to the Verified Software Initiative. |
Collaborator Contribution | Suppliers of case studies, verification technology, challenge project prizes, organisers of workshops. |
Impact | Collection of verification case studies for experimentation by the verification community. |
Start Year | 2006 |
Description | VSR collaborations |
Organisation | Praxis Systems Ltd |
Country | United Kingdom |
Sector | Private |
PI Contribution | Organising the UK's contribution to the Verified Software Initiative. |
Collaborator Contribution | Suppliers of case studies, verification technology, challenge project prizes, organisers of workshops. |
Impact | Collection of verification case studies for experimentation by the verification community. |
Start Year | 2006 |
Description | bangalore-2018 |
Organisation | Indian Institute of Science Bangalore |
Country | India |
Sector | Academic/University |
PI Contribution | Newton grant from RAEng held by IIIT-B. Contributions on refinement of simulink models. |
Collaborator Contribution | Research in refinement of simulink models. |
Impact | Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock: Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. RAMiCS 2018: 205-224 Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock: Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. CoRR abs/1806.02101 (2018) |
Start Year | 2018 |
Description | butterfield-tcd-march-2018 |
Organisation | Trinity College Dublin |
Department | Trinity Biomedical Sciences Institute |
Country | Ireland |
Sector | Hospitals |
PI Contribution | Research discussions at TCD. |
Collaborator Contribution | Research discussions. |
Impact | Discussions on future research collaborations. |
Start Year | 2018 |
Description | chongqing-2-2018 |
Organisation | Southwest University |
Country | China |
Sector | Academic/University |
PI Contribution | Royal Society China Cost Share Programme |
Collaborator Contribution | Research contributions. |
Impact | None yet. |
Start Year | 2018 |
Description | chongqing2018 |
Organisation | Southwest University |
Country | China |
Sector | Academic/University |
PI Contribution | Royal Society China Cost Share Programme. |
Collaborator Contribution | Rsearch contributions. |
Impact | No outputs yet. |
Start Year | 2018 |
Description | digit-2018 |
Organisation | Aarhus University |
Department | Aarhus Institute of Advanced Studies |
Country | Denmark |
Sector | Academic/University |
PI Contribution | Planning for future collaboration. |
Collaborator Contribution | Research exchanges. |
Impact | Proposal to Grundfos Foundation. |
Start Year | 2018 |
Description | peleska-testing-2018 |
Organisation | University of Bremen |
Country | Germany |
Sector | Academic/University |
PI Contribution | Rsearch discussions. |
Collaborator Contribution | Rsearch discussions. |
Impact | Research proposals. |
Start Year | 2018 |
Title | Mechanised Unifying Theories of Programming |
Description | Mechanisation of a framework for reasoning about notations and techniques for refinement. The concept was developed on an industrial theorem prover, ProofPower-Z, adopted by our industrial collaborator. More recently, we have implemented the design using a theorem prover of more general use: Isabelle. It has been used in an EU project to verify Systems of Systems. |
Type Of Technology | Software |
Year Produced | 2010 |
Open Source License? | Yes |
Impact | It has been relevant for all our research and will continue to support our work, as we consider different areas of application: robotics, medical devices, and so on. |
Description | CyPhyAssure Spring School |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Participation in Spring School on the assurance of cyber-physical systems. |
Year(s) Of Engagement Activity | 2019 |
URL | https://www.cs.york.ac.uk/circus/CyPhyAssure/school/ |
Description | DIGIT Advisory Board |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Participation in the advisory board of the center for digital twins at Aarhus University, |
Year(s) Of Engagement Activity | 2018 |
Description | FM 2019 |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Talks and discussions with international colleagues. |
Year(s) Of Engagement Activity | 2019 |
Description | Hay Festival session |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | National |
Primary Audience | Public/other audiences |
Results and Impact | More than 300 people attended, and the presentation sparked many questions and discussion afterwards. I have been asked by the Royal Society to participate of a campaign to encourage colleagues to engage with the public. |
Year(s) Of Engagement Activity | 2013 |
Description | Huawei Research Forum |
Form Of Engagement Activity | A formal working group, expert panel or dialogue |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | Presentation on formal methods for assurance of security-related software in Huawei 5G products. |
Year(s) Of Engagement Activity | 2019 |
Description | Huawei Research Symposium |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | Presentation of my research agenda to Huawei engineers. I gave advice on future research policy for their company. |
Year(s) Of Engagement Activity | 2019 |
Description | IFIP WG 2.3 Programming Methodology |
Form Of Engagement Activity | A formal working group, expert panel or dialogue |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Hosted meeting of IFIP WG 2.3 on Programming Methodology. Organised scientific and social agenda, chaired the meeting, and gave an extended scientific talk. I involved my doctoral students and research assistants in the meeting. |
Year(s) Of Engagement Activity | 2019 |
URL | https://ifip-tc2-wg23.paluno.uni-due.de/?page_id=455 |
Description | Newton Institue Workshop |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | I gave a talk about the impact of verification technology on practical application. |
Year(s) Of Engagement Activity | 2019 |
Description | Open Day |
Form Of Engagement Activity | Participation in an open day or visit at my research institution |
Part Of Official Scheme? | No |
Geographic Reach | Local |
Primary Audience | Schools |
Results and Impact | Presentation of robotic applications developed using our techniques. |
Year(s) Of Engagement Activity | 2016 |
Description | Opening of Aarhus Centre for Digital Twins |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | Keynote talk on research direction at the opening of the Centre for Digital Twins at Aarhus University. |
Year(s) Of Engagement Activity | 2019 |
URL | https://digit.au.dk/research-projects/centre-for-digital-twins/ |
Description | Spring School on Engineering Trustworthy Software Systems |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | Spring School on Engineering Trustworthy Software Systems (SETSS), held in April, 2016, at Southwest University in Chongqing, China. The school was aimed at post-graduate students, researchers, academics, and industrial engineers who are interested in the theory and practice of methods and tools for the design and programming of trustworthy software systems. |
Year(s) Of Engagement Activity | 2016 |
Description | Symposium for Marie-Claude Gaudel |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | I gave a talk on software engineering for robotic control. |
Year(s) Of Engagement Activity | 2019 |
Description | Talk at Verification Future Meeting |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | National |
Primary Audience | Industry/Business |
Results and Impact | I gave an invited talk at this industry meeting. |
Year(s) Of Engagement Activity | 2019 |
URL | https://www.testandverification.com/conferences/verification-futures/vf2019 |
Description | Visit by Jan Pekeska |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | Discussions on research collaboration. |
Year(s) Of Engagement Activity | 2018 |
Description | Visit by Ziming Liiu |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Visit to discuss long-term research collaboration. |
Year(s) Of Engagement Activity | 2018 |
Description | Visit from Southwest University |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Visit from a delegation from Southwest University, Chongqing, China. |
Year(s) Of Engagement Activity | 2019 |
Description | Visit from TCD Ireland |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | Visit from colleagues from Trinity College Dublin. Contributions on probabilistic semantic for robotics. |
Year(s) Of Engagement Activity | 2018,2019 |
Description | Visit ti Aarhus University |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Visit to exchange research ideas. |
Year(s) Of Engagement Activity | 2018 |
Description | Visit to Chongqing |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Visit Southwest University to give lectures and direct doctoral students. |
Year(s) Of Engagement Activity | 2019 |
Description | Visit to Chongqing |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | Workshop on formal methods for human-cyber-=physical systems. I gave talks on software engineering for robotics. |
Year(s) Of Engagement Activity | 2019 |
Description | Visit to IISc |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Presentation of research work. Exchange of research ideas for future research proposals. |
Year(s) Of Engagement Activity | 2018 |
Description | Visit to IISc Bangalore |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Workshop at IISc funded by Royal Academy of Engineering. Discussed work on formal verification of operating system real-time kernels. |
Year(s) Of Engagement Activity | 2019 |
Description | Visit to Malardalen University |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | External examining of a doctoral student. Interaction with academic colleagues on research directions. Interaction with industry colleagues on research directions. |
Year(s) Of Engagement Activity | 2019 |
Description | Visit to Southwest University |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Visit to exchange ideas. |
Year(s) Of Engagement Activity | 2018 |
Description | White Rose Retreat on Robotics |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | Local |
Primary Audience | Study participants or study members |
Results and Impact | Discussed future collaborative in robotics. |
Year(s) Of Engagement Activity | 2019 |