International audience

In the aftermath of COVID-19, remote working has become the norm, and graduates now need an even wider range of skills, which traditional classrooms and internships do not always provide. Working in multiple time zones, within global multi-cultural teams, and only ever meeting colleagues through online technology are just some of the challenges, which require a new type of global graduate. Transversal skills including leadership, collaboration, innovation, digital, green, organization and communication skills are critical. The disruption from COVID-19 also presents unprecedented opportunities to develop more inclusive approaches to internships and international experiences, to level the playing field for students with special needs, from underrepresented groups or with caring commitments. In this position paper, we present a new Global Innovation internship model that has the aim of allowing students to complete technology internships and projects by working together virtually on real world challenges, guided by experienced industry and academic mentors. The model is being developed as part of an Erasmus+ funded project, and the partnership includes seven Higher Education Institutions from six different countries around the world. This position paper describes the design and development of a pilot programme of the Global Innovations internship model.

Cyber-Physical Systems (CPSs) [ 1 ] connect the real world to software systems through a network of sensors and actuators in which physical and logical components interact in complex ways. There is a diverse range of application domains [ 2 ], including health [ 3 ], energy [ 4 ], transport [ 5 ], autonomous vehicles [ 6 ] and robotics [ 7 ]; and many of these include safety critical requirements [ 8 ]. Such systems are, by definition, characterised by both discrete and continuous components. The development and verification processes must, therefore, incorporate and integrate discrete and continuous models. The development of techniques and tools to handle the correct design of CPSs has drawn the attention of many researchers. Continuous modelling approaches are usually based on a formal mathematical expression of the problem using dense reals and differential equations to model the behaviour of the studied hybrid system. Then, models are simulated in order to check required properties. Discrete modelling approaches rely on formal methods, based on abstraction, model-checking and theorem proving. There is much ongoing research concerned with how best to combine these approaches in a more coherent and pragmatic fashion, in order to support more rigorous and automated hybrid-design verification. It is also possible to combine different discrete-event and continuous-time models using a technique called co-simulation. This has been supported by different tools and the underlying foundation for this has been analysed. Thus, the track will also look into these areas as well as the industrial usage of this kind of technology.

A Software Product Line (SPL) is a tool/method used to generate a family of program/system variants for a specific domain, and to support a more efficient software development of future products within the same domain. A Feature Model (FM) is a popular graphical/textual representation used in SPL requirements specification; it is used to capture commonality and variability information existing in an SPL as a set of inter-related and configurable features. A concrete model of an SPL instance is obtained by binding the variation information in the FM with a configuration that meets a specific set of feature requirements. Since configuration decisions are taken prior to instantiation, invalid configurations should be detected/avoided before design begins. This paper addresses the problem of the verification of the correctness (validity) of FM instances and FM configuration during requirements modelling. It proposes a requirements model based on Event-B contexts, allowing us to check the correctness of a given configuration, before starting the correct-by-construction design and implementation process, based on refinement.

In mobile crowdsensing (MCS), one of the participants' main concerns is the cost for 3G data usage, which affects their willingness to participate in a crowdsensing task. In this paper, we present the design and implementation of an MCS data uploading mechanism-ecoSense-to help reduce additional 3G data cost incurred by the whole crowd of sensing participants. By considering the two most common real-life 3G price plans-unlimited data plan (UnDP) and pay as you go (PAYG), ecoSense partitions all the users into two groups corresponding to these two price plans at the beginning of each month, with the objective of minimizing the total refunding budget for all participants. The partitioning is based on predicting users' mobility patterns and sensed data size. The ecoSense mechanism is designed inspired by the observation that during the data uploading cycles, UnDP users could opportunistically relay PAYG users' data to the crowdsensing server without extra 3G cost, provided the two types of users are able to “meet” on a common local cost-free network (e.g., Bluetooth or WiFi direct). We conduct our experiments using both the Massachusetts Institute of Technology reality mining and the Small World In Motion (SWIM) simulation data sets. Evaluation results show that ecoSense could reduce total 3G data cost by up to ~50%, when compared to the direct-assignment method that assigns each participant to UnDP or PAYG directly according to the size of her sensed data.

Mobile Crowdsensing (MCS) requires users to be motivated to participate. However, concerns regarding energy consumption and privacy—among other things—may compromise their willingness to join such a crowd. Our preliminary observations and analysis of common MCS applications have shown that the data transfer in MCS applications may incur significant energy consumption due to the 3G connection setup. However, if data are transferred in parallel with a traditional phone call, then such transfer can be done almost “for free”: with only an insignificant additional amount of energy required to piggy-back the data—usually incoming task assignments and outgoing sensor results—on top of the call. Here, we present an Energy-Efficient Mobile Crowdsensing (EEMC) framework where task assignments and sensing results are transferred in parallel with phone calls. The main objective, and the principal contribution of this article, is an MCS task assignment scheme that guarantees that a minimum number of anonymous participants return sensor results within a specified time frame, while also minimizing the waste of energy due to redundant task assignments and considering privacy concerns of participants. Evaluations with a large-scale real-world phone call dataset show that our proposed EEMC framework outperforms the baseline approaches, and it can reduce overall energy consumption in data transfer by 54--66% when compared to the 3G-based solution.

We report on our experiences in teaching graph theory and algorithms to school children, aged 5 to 17. Our objectives were to demonstrate that children can discover quite complex mathematical concepts, and are able to work with abstractions and use computation reasoning from quite an early age. We provide details of our incremental approach, which can be used with students of a wide range of abilities. Also, we comment on the importance of problem based learning where the algorithms are presented as possible solutions to games or puzzles. Finally, we conclude with a number of important observations with regard to the introduction of computer science into schools.

In general, university guidelines or policies on plagiarism are not sufficiently detailed to cope with the technical complexity of software. Software plagiarism can have a significant impact on a student's degree result, particularly in courses were there is a significant emphasis on large-scale projects. We argue that a policy for software reuse is the most explicit, and fair, way of overcoming this problem. In our policy, we specify the notion of software to cover all the documents that are generally built during the engineering of a software system -- analysis, requirements, validation, design, verification, implementation and tests. Examples are used to show acceptable and unacceptable forms of reuse, mostly at the design, testing and implementation stages. These examples are represented in Java, although they should be easily understood by anyone with software engineering experience. We conclude with a simple code of practice for reuse of software based on a file-level policy, combined with emphasis on re-using only what is rigorously verified.

In this paper we propose that formal modelling techniques are necessary in establishing the trustworthiness of e-voting systems and the software within. We illustrate how a distributed e-voting system architecture can be analysed against quality of service requirements, through simulation of formal models. A concrete example of a novel e-voting system prototype (for use in french elections) is used to justify the utility of our approach. The quality of service that we consider is the total time it takes for a voter to record their vote (including voting time)/ The innovative aspects of the e-voting system that required further research were new requirements for voting anywhere and re-voting; and the potential for undesirable interactions between them.

The storage of votes is a critical component of any voting system. In traditional systems there is a high level of transparency in the mechanisms used to store votes, and thus a reasonable degree of trustworthiness in the security of the votes in storage. This degree of transparency is much more difficult to attain in electronic voting systems, and so the specific mechanisms put in place to ensure the security of stored votes require much stronger verification in order for them to be trusted by the public. There are many desirable properties that one could reasonably expect a vote store to exhibit. From the point of view of security, we argue that tamper-evident storage is one of the most important requirements: the changing, or deletion of already validated and stored votes should be detectable; as should the addition of unauthorised votes after the election is concluded. We propose the application of formal methods (in this paper, event- B) for guaranteeing, through construction, the correctness of a vote store with respect to the requirement for tamper- evident storage. We illustrate the utility of our refinement- based approach by verifying - through the application of a reusable formal design pattern - a store design that uses a specific PROM technology and applies a specific encoding mechanism.

The fundamental principle behind Problem-based Learning (PBL) is that the problem is the driving force that initiates the learning. In order to function effectively in a PBL environment a good set of problems is required. Solving problems is a vital element within Computer Science and yet the discipline has been slow to embrace PBL as an approach to learning. The net result means that there are few good PBL problems available to assist new practitioners with implementation. PBL emphasizes a real-world approach to learning, and we present a RoboCode Competition as a candidate for a good, realistic PBL problem within the computer science discipline. We list and identify the criteria that categorise a PBL problem as good and validate the RoboCode domain against these criteria. We argue that the concept of freedom --- in different guises --- plays a key role in making PBL a good mechanism for teaching programming, and for making RoboCode a good domain for PBL.

This paper proposes a model which explains the process of learning about computation in terms of well-accepted software engineering concepts, and argues that our approach to understanding how problem-solving skills are acquired is an innovation over well-accepted learning theories and models. It examines how it all students make sense of computational processes; by reporting on experimental observations that have been made with school children, and with university undergraduates. We observed little difference between children and adults with regard to how they learn about computation, and suggest that the strong similarities are due to a common set of problem-solving techniques which are fundamental to all problem based learning, in general, and learning about computation, in particular. To conclude, we demonstrate that our model --- based on software engineering concepts --- is useful when reasoning about the relationship between problem solving and learning to program.

This paper describes the use of random code generation and mutation as a method for synthesising multiple choice questions which can be used in automated assessment. Whilst using multiple choice questions has proved to be a feasible method of testing if students have suitable knowledge or comprehension of a programming concept, creating suitable multiple choice questions that accurately test the students' knowledge is time intensive.This paper proposes two methods of generating code which can then be used to closely examine the comprehension ability of students. The first method takes as input a suite of template programs, and performs slight mutations on each program and ask students to comprehend the new program. The second method performs traversals on a syntax tree of possible programs, yielding slightly erratic but compilable code, again with behaviour that students can be questioned about. As well as generating code these methods also yield alternative distracting answers to challenge the students. Finally, this paper discusses the gradual introduction of these automatically generated questions as an assessment method and discusses the relative merits of each technique.

The size and complexity of hardware and software systems continues to grow, making the introduction of subtle errors a more likely possibility. A major goal of software engineering is to enable developers to construct systems that operate reliably despite increased size and complexity. One approach to achieving this goal is through formal methods: mathematically based languages, techniques and tools for specifying and verifying complex software systems. The authors apply a theoretical tool (that is supported by many formal methods), the correctness preserving transformation (CPT), to a real software engineering problem: the need for optimization during the maintenance of code. We present four program transformations and a model that forms a framework for proof of correctness. We prove the transformations correct and then apply them to a cryptography application implemented in C++. Our experience shows that CPTs can facilitate generation of more efficient code while guaranteeing the preservation of original behavior.