Model checking has often been used for verifying Cyber-Physical Systems (CPS). A major challenge is how to capture a model that represents the actual behavior of the software. Model extraction can introduce errors that can affect the accuracy of the analysis including loss of precision, inconsistency, non-conformance, and over- and under-approximations. In this paper, we formalize and prove the correctness of extracting a model from a subset of the MicroPython programming language with respect to a trace-based semantics. The extracted models capture the order of method calls and can be model checked using Shelley. We formalize the extraction process from an intermediate representation of MicroPython codes and prove that the behavior of our intermediate representation is a regular language. Our formalization and theoretical results are fully mechanized using the Coq proof assistant.

Developing critical software requires adherence to rigorous software development practices, such as formal requirement specification and verification. Despite their importance, such practices are often considered as complex and challenging tasks that require a strong formal methods background. In this paper, we present our work on simplifying the formal requirements specification experience for resource-constrained mission critical software through the use of structured natural language. To this end, we connect NASA’s FRET, a formal requirement elicitation and authoring tool with the Shelley model checking framework for MicroPython code. We report our experience on using these tools to specify requirements and analyze code from the NASA Ames PHALANX exploration concept.

This paper introduces Shelley, a novel model checking framework used to verify the order of function calls, developed in the context of Cyber-Physical Systems (CPS). Shelley infers the model directly from MicroPython code, so as to simplify the process of checking requirements expressed in a temporal logic. Applications for CPS need to reason about the end of execution to verify the reclamation/release of physical resources, so our temporal logic is stated on finite traces. Lastly, Shelley infers the behavior from code using an inter-procedural and compositional analysis, thus supporting the usual object-oriented programming techniques employed in MicroPython code. To evaluate our work, we present an experience report on an industrial application and evaluate the bounds of the validity checks (up to $$12^{12}$$ subsystems under 10 s on a desktop computer).

We presentParTypes, a type discipline for parallel programs. The model we have in mind comprises a fixed number of processes running in parallel and communicating via collective operations or point-to-point synchronous message exchanges. A type describes a protocol to be followed by each processes in a given program. We present the type theory, a core imperative programming language and its operational semantics, and prove that type checking is decidable (up to decidability of semantic entailment) and that well-typed programs do not deadlock and always terminate. The article is accompanied by a large number of examples drawn from the literature on parallel programming.

The context information that business process can get from the Internet of Things (IoT) can be used as a competitive advantage in terms of optimisation and agility. However, the exchange of messages between central systems and IoT devices come with a price, battery consumption, a scarcely resource of such devices. Despite the literature offers many technical proposals to tackle this problem, we take an approach driven by the process definition perspective. We propose to reduce the number of exchanged messages by decentralising process execution, moving parts of the business processes to IoT devices, and taking advantage of their computational capabilities. The first step for decentralisation is decomposition, i.e., the division of processes into parts and identify those that IoT devices can execute. In this paper, we present an automatic decomposition solution for IoT aware business processes, described using the Business Process Model and Notation (BPMN). We start from a BPMN definition that follows a centralised approach and apply our decomposition method to transfer to the IoT devices the operations that can be performed there. We use a graph based approach and transform a BPMN definition into a directed graph. Thereafter, we identify cuts that define the parts to be transferred to the IoT devices. This decomposition preserves the control and the data dependencies of the original process, reduces the number of exchanged messages as well as the central processing. The code that IoT devices execute is automatically generated from the BPMN process being decentralised.

Web programming is a mandatory course in the syllabus of any BSc degree in Informatics Engineering. But, nowadays, designing and teaching an up-to-date web programming course is a very demanding challenge due to the fast technological advances that imposes a continuous update of the concepts, techniques, and tools. Nowadays, from a professional perspective, web development is starting to converge on merging front-end and back-end development. This requires new skills for web developers, traditionally separated into two groups (front-end and back-end), that are still not accompanied by academia web programming courses. This future trend motivates us for designing a higher education course that combines Web design and server-side programming skills in a unified full-stack of Web technologies to develop modern web applications. The paper intends to present and discuss a new higher education course for a curricular unit in Web programming of a degree in Informatics in the European higher education system. The course is aligned with the new trends, providing students with fundamentals and basic skills in the development of Web applications, using the full-stack approach to Web development supported by the MEAN stack architecture.

The Internet of Things (IoT) is generally seen as a distributed information gathering platform when used in business processes (BP). IoT devices have computational capabilities that can and should be used to execute fragments of BP that present benefits for both the devices and the BP execution engine. In fact, executing parts of the BP in the IoT devices may result in the reduction of the number of messages exchanged between the IoT network and the BP execution engine, increasing the battery lifespan of the IoT devices; also, it reduces the workload of the BP execution engine. However, processes are still defined following a centralised approach, making it difficult to use the full capabilities of these devices. In this paper, we present an automatic decomposition solution for IoT aware business processes, described using the Business Process Model and Notation (BPMN). We start from a BP model that follows a centralised approach and apply our decomposition method to transfer to the IoT devices the operations that can be performed there. This transformation preserves the control and the data flows of the original process and reduces the central processing and the number of messages exchanged in the network. The code that IoT devices execute is automatically generated from the BPMN process being decentralised.

Representational State Transfer (REST), an architectural style providing an abstract model of the web, is by far the most popular platform to build web applications. Developing such applications require well-documented interfaces. However, and despite important initiatives such as the Open API Specification, the support for interface description is currently quite limited, focusing essentially on simple syntactic aspects. In this paper we present HeadREST, a dependently-typed language that allows describing semantic aspects of interfaces in a style reminiscent of Hoare triples.

Due to its particular features, LoRa is gaining more and more attention from industry and academia because it tries to combine long communication range, low-power consumption, and low-data rate application. A very important feature observed on LoRa is that it is highly robust and reliable. Due to this, LoRa is being applied in many IoT solutions in urban environment, but on hard natural environments like dense forest, near river sides, lakes and mangroves, more studies need to be carried out in order to evaluate the its quality. This paper describes experimental studies carried out to measure LoRa communication range and Received Signal Strength Indicator (RSSI), both in natural and urban environments. The experiments took place in two different places of the world, one in the northern hemisphere and another in the southern hemisphere: on the Portuguese archipelago of the Azores (in SãoMiguel Island) and in the city of João Pessoa in Northeast of Brazil, respectively. As a result, we observed that LoRa is very robust in dense urban environments, where it was possible to established long distance connections (approximately 2.1 km). However, the results were inconclusive in forest environments, because in the Azores, the LoRa connection ranged about 800 m thought the forest/lake, while in Brazil it was about 230 m.

The continuous global growth of urban population increased the waste generation rate in cities. Garbage collection became one of the most important services each city hall offers to protect its inhabitants and the environment from the harmful impact of solid waste. In this paper, we present a prototypical device that measures the filling level of a waste bin using Infrared based sensors. Most of the state-of-the-art market products use ultrasonic sensors, a technology twice as expensive as the one we propose. We created an Internet of Things (IoT) device capable of computing a bins' filling level (<; 25%, <; 50%, <; 75%, > 75%. and estimate the occupied volume inside the container using a set of infrared emitters and receivers. We also report on the results of the experiments with our device in a real world scenario.

Modern hardware platforms, from the very small to the very large, increasingly provide parallel and distributed computing resources for applications to maximise performance. Many applications therefore need to make effective use of tens, hundreds, and even thousands of compute nodes. Computation in such systems is thus inherently concurrent and communication centric. Effectively programming such applications is challenging; performance, correctness, and scalability are difficult to achieve. The development of effective programming methodologies for this increasingly parallel landscape therefore demands exploration and understanding of a wide variety of foundational and practical ideas. The International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES) is dedicated to work in this area. The workshop offers a forum for researchers from different fields to exchange new ideas about these challenges to modern and future programming, where concurrency and distribution are the norm rather than a marginal concern. This proceedings covers the 11th edition of PLACES, which was co-located with ETAPS 2019 in Prague, Czech Republic.

This chapter presents the PARTYPES framework to statically verify C programs that use the Message Passing Interface, the widely used standard for message-based parallel applications. Programs are checked against a protocol specification that captures the interaction in an MPI program. The protocol language is based on a dependent type system that is able to express various MPI communication primitives, including point-to-point and collective operations. The verification uses VCC, a mechanical verifier for concurrent C programs. It takes the program protocol written in VCC format, an annotated version of the MPI library, and the program to verify, and checks whether the program complies with the protocol.

As the computational power of IoT (Internet of Things) devices increases, business processes can use them to provide information about real world as well as to execute part of business processes, reducing the amount of exchanged data and central processing. Current BPMN-based approaches already support modellers to define both business processes and IoT devices behaviour at the same level of abstraction. However, they are not restricted to standard BPMN elements and they generate IoT device specific low-level code. The work we present in this paper only uses standard BPMN to define both central and IoT behaviour of business processes. In addition, the BPMN that defines the IoT behaviour is translated to a neutral-platform programming code.

The Message Passing Interface (MPI) framework is widely used in implementing imperative programs that exhibit a high degree of parallelism.The PARTYPES approach proposes a behavioural type discipline for MPI-like programs in which a type describes the communication protocol followed by the entire program.Well-typed programs are guaranteed to be exempt from deadlocks.In this paper we describe a type inference algorithm for a subset of the original system; the algorithm allows to statically extract a type for an MPI program from its source code.

Futures are an elegant approach to expressing parallelism in functional programs. However, combining futures with imperative programming (as in C++ or in Java) can lead to pernicious bugs in the form of data races and deadlocks, as a consequence of uncontrolled data flow through mutable shared memory. In this paper we introduce the Known Joins (KJ) property for parallel programs with futures, and relate it to the Deadlock Freedom (DF) and the Data-Race Freedom (DRF) properties. Our paper offers two key theoretical results: 1) DRF implies KJ, and 2) KJ implies DF. These results show that data-race freedom is sufficient to guarantee deadlock freedom in programs with futures that only manipulate unsynchronized shared variables. To the best of our knowledge, these are the first theoretical results to establish sufficient conditions for deadlock freedom in imperative parallel programs with futures, and to characterize the subset of data races that can trigger deadlocks (those that violate the KJ property). From result 2), we developed a tool that avoids deadlocks in linear time and space when KJ holds, i.e., when there are no data races among references to futures. When KJ fails, the tool reports the data race and optionally falls back to a standard deadlock avoidance algorithm by cycle detection. Our tool verified a dataset of ∼2,300 student’s homework solutions and found one deadlocked program. The performance results obtained from our tool are very encouraging: a maximum slowdown of 1.06× on a 16-core machine, always outperforming deadlock avoidance via cycle-detection. Proofs of the two main results were formalized using the Coq proof assistant.

This chapter presents the PARTYPES framework to statically verify C programs that use the Message Passing Interface, the widely used standard for message-based parallel applications. Programs are checked against a protocol specification that captures the interaction in an MPI program. The protocol language is based on a dependent type system that is able to express various MPI communication primitives, including point-to-point and collective operations. The verification uses VCC, a mechanical verifier for concurrent C programs. It takes the program protocol written in VCC format, an annotated version of the MPI library, and the program to verify, and checks whether the program complies with the protocol.

Whereas, traditionally, business processes use the Internet of Things (IoTs) as a distributed source of information, the increase of computational capabilities of IoT devices provides them with the means to also execute parts of the business logic, reducing the amount of exchanged data and central processing. Current approaches based on Business Process Model and Notation (BPMN) already support modelers to define both business processes and IoT devices behavior at the same level of abstraction. However, they are not restricted to standard BPMN elements and they generate IoT device specific low-level code. The work we present in this paper exclusivelly uses standard BPMN to define central as well as IoT behavior of business processes. In addition, the BPMN that defines the IoT behavior is translated to a neutral-platform programming code. The deployment and execution environments use Web services to support the communication between the process execution engine and IoT devices.

Wireless sensor networks are notoriously difficult to program and debug. This fact not only stems from the nature of the hardware, but also from the current approaches for developing programming languages and runtime systems for these platforms. In particular, current systems do not place enough stress on providing formal descriptions of the language and its runtime system, and on proving static properties, like type-safety and soundness. In this paper, we present the design, specification, and implementation of a programming language and a runtime system for wireless sensor networks that are safe by design. We say this in the sense that we can statically detect a large set of would-be runtime errors, and that the runtime system will not incorrectly execute an application, once the latter is deployed. We have a full prototype implementation of the system that supports SunSPOT devices, the simulation tool VisualSense, and local computer networks for fast deployment and testing of applications. Development is supported by an IDE implemented on top of the Eclipse tool that embeds both the compiler and the virtual machine seamlessly, and is used to produce software releases.