Marine in-situ data is collected by sensors mounted on fixed or mobile systems deployed into the ocean. This type of data is crucial both for the ocean industries and public authorities, e.g., for monitoring and forecasting the state of marine ecosystems and/or climate changes. Various public organizations have collected, managed, and openly shared in-situ marine data in the past decade. Recently, initiatives like the Ocean Decade Corporate Data Group have incentivized the sharing of marine data of public interest from private companies aiding in ocean management. However, there is no clear understanding of the impact of data quality in the engineering of systems, as well as on how to manage and exploit the collected data. In this paper, we propose main architectural decisions and a data flow-oriented component and connector view for marine in-situ data streams. Our results are based on a longitudinal empirical software engineering process, and driven by knowledge extracted from the experts in the marine domain from public and private organizations, and challenges identified in the literature. The proposed software architecture is instantiated and exemplified in a prototype implementation.

The ocean is vital for humankind but may cause catastrophes when unhealthy. Although there have been efforts to build ocean monitoring systems, the understanding of the underwater environment is limited due to the cost and challenges of obtaining real-time marine data. One potential solution is to build stationary ocean observation systems based on wireless communication due to its affordable cost. In this study, we divide these systems into three components: 1) underwater data acquisition; 2) network communication; and 3) data management. We investigate the engineering challenges associated with each component, the causes, and how they relate. The literature has not discussed the technical issues of building stationary smart ocean monitoring systems entirely based on wireless communication yet. This article fills that research gap by conducting semi-structured interviews with 17 experts knowledgeable about underwater sensors, underwater acoustic communication, offshore network communication, and underwater data usage. The identified challenges are compared with the literature to assess whether our findings are novel or are a confirmation of what have been already found in prior publications. The Internet of Things (IoT) used in smart city platforms is quite advanced, but the Internet of Underwater Things (IoUT) employed in smart ocean monitoring systems has several unresolved issues; although IoT is viewed as a foundation for IoUT. Therefore, we compare fundamental differences between the technologies used in the smart city and the smart ocean domains, explaining why some of our identified challenges are unique in the marine context.

The inherent computational complexity of validating and verifying concurrent systems implies a need to be able to exploit parallel and distributed computing architectures. We present a new distributed algorithm for state space exploration of concurrent systems on computing clusters. Our algorithm relies on Remote Direct Memory Access (RDMA) for low-latency transfer of states between computing elements, and on state reconstruction trees for compact representation of states on the computing elements themselves. For the distribution of states between computing elements, we propose a concept of state stealing. We have implemented our proposed algorithm using the OpenSHMEM API for RDMA and experimentally evaluated it on the Grid'500 testbed with a set of benchmark models. The experimental results show that our algorithm scales well with the number of available computing elements, and that our state stealing mechanism generally provides a balanced workload distribution.

Knowing vegetation type in an area is crucial for several applications, including ecology, land use management, and infrastructure risk assessment. In combination with recent advancements in image processing, remote sensing technology has been used to perform fast vegetation type estimation and reduce the need for intensive and time-consuming field-based surveys. This paper proposes a weakly supervised method based on deep learning to estimate tree species relying on multi-spectral high-resolution satellite images. We tested the approach against noisy labels, which often occur in real-world datasets. We validate our approach for a study area in Norway and in Italy using images taken in different periods of the year. Our method significantly enhances the quality of the available forestry inventory dataset.

Vegetation is one of the primary causes of outages in electricity transmission and distribution networks and represents a significant expense in maintaining a power grid. While LiDAR or multi-view images can be used for detecting vegetation along power lines, such technologies are costly and difficult to acquire to cover widespread electricity networks. This paper proposes a framework for 3D mapping of trees along power lines using monocular high-resolution satellite images. Such type of imagery has become nowadays affordable and easy to acquire. Furthermore, single snapshots can cover a large portion of the grid in high revisiting time. We train and test different state-of-the-art models to map the contextual information from images into a height prediction. We validate our proposed satellite-based framework for an electricity distribution network in the western part of Norway using actual LiDAR data.

This paper presents a search-based approach relying on multi-objective reinforcement learning and optimization for test case generation in model-based software testing. Our approach considers test case generation as an exploration versus exploitation dilemma, and we address this dilemma by implementing a particular strategy of multi-objective multi-armed bandits with multiple rewards. After optimizing our strategy using the jMetal multi-objective optimization framework, the resulting parameter setting is then used by an extended version of the Modbat tool for model-based testing. We experimentally evaluate our search-based approach on a collection of examples, such as the ZooKeeper distributed service and PostgreSQL database system, by comparing it to the use of random search for test case generation. Our results show that test cases generated using our search-based approach can obtain more predictable and better state/transition coverage, find failures earlier, and provide improved path coverage.

Abstract: Distributed systems modelling often involves a set of heterogeneous models where each model specifies a set of local constraints capturing a specific view of the system. In real life, distributed systems are often loosely connected and interdependencies are not defined into their software model. This limits the scope of optimization of distributed resources. In this paper, we merge heterogeneous models of distributed systems and articulate distributed resource constraints via inter-metamodel constraints. We apply model-driven engineering and use model transformation rules to construct an epistemic game theory model for the purpose of optimizing distributed resource allocation. Since the application of transformation rules normally do not guarantee the satisfaction of constraints when applied on a model, it requires a conformance checking which is an expensive operation. To overcome this problem, we introduce the concept of compliant rule and coordinate with other rules for efficient m (More) \nPublished with permission from SciTePress. Copyright 2017 by SCITEPRESS – Science and Technology Publications, Lda. All rights reserved.

TinyOS is a widely used platform for the development of networked embedded systems offering a programming model targeting resource constrained devices. We present a semi-automatic software engineering approach where Coloured Petri Net (CPNs) models are used as a starting point for developing protocol software for the TinyOS platform. The approach consists of five refinement steps that allow a developer to gradually transform a platform-independent CPN model into a platform-specific model that enables automatic code generation. To evaluate our approach, we use it to obtain an implementation of the IETF RPL routing protocol for sensor networks. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Metamodelling and model transformation play important roles in model-driven engineering as they can be used to define domain-specific modelling languages. During the modelling phase, modellers encode domain knowledge into models which may include both structural and behavioral aspects of a system. The contribution of this paper is a new web-based metamodelling and model transformation tool called WebDPF based on the Diagram Predicate Framework (DPF). WebDPF supports multilevel diagrammatic metamodelling and specification of model constraints, and it supports diagrammatic development and analysis of model transformation systems. We show how the support for model transformation systems in WebDPF can be exploited to (i) support auto-completion of partial models thereby enhancing modelling efficiency, and (ii) provide execution semantics for workflow models. Furthermore, we illustrate how WebDPF incorporates a scalable model navigation facility designed to enable users to inspect and query large models.

The sweep-line method allows explicit state model checkers to delete states from memory on-the-fly during state space exploration, thereby lowering the memory demands of the verification procedure. The sweep-line method is based on a least-progress-first search order that prohibits the immediate use of standard on-the-fly Büchi automata-based model checking algorithms that rely on a depth-first search order in the search for an acceptance cycle. This paper proposes and experimentally evaluates an algorithm for Büchi automata-based model checking compatible with the search order and deletion of states prescribed by the sweep-line method.

This special issue is dedicated to selected papers from the 32nd International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, which took place in June 2011 in Newcastle upon Tyne, UK.In a careful reviewing process, 17 regular contributions have been accepted for presentation at the conference among 49 submissions.Then, after the conference, a collection of papers published in the proceedings was selected with the help of the Program Committee members, and the authors were invited to revise and extend their contributions for this special issue.Next, the extended submissions have been examined in another independent reviewing process involving two review rounds to meet the standards of FUNDAMENTA INFORMATICAE.Finally, six contributions have been accepted for publication.The accepted papers give a good overview of some recent developments in the area of Petri nets and other models of concurrency.

The Generic Access Network (GAN) architecture is defined by the 3rd Generation Partnership Project (3GPP) and allows telephone services, such as SMS and voice-calls, to be accessed via Internet Protocol (IP) networks. The main usage of this is to allow mobile phones to use WiFi in addition to the usual GSM network. The GAN specification relies on the Internet Protocol Security layer (IPSec) and the Internet Key Exchange protocol (IKEv2) to provide encryption across IP networks, and thus avoid compromising the security of the telephone networks. The detailed usage of these two Internet protocols (IPSec and IKEv2) is not fully described in the GAN specification. As part of the process to develop solutions to support the GAN architecture, TietoEnator Denmark has developed a detailed GAN scenario which describes how IPSec and IKEv2 are to be used during the connection establishment procedure. This paper presents an industrial project where Coloured Petri Nets (CPNs) were used to specify and validate the detailed GAN scenario considered by TietoEnator.

State-space exploration is one of the main approaches to computer-aided verification and analysis of finite-state systems. It is used to reason about a wide range of properties during the design phase of a system, including system deadlocks. Unfortunately, state-space exploration needs to handle huge state spaces for most practical systems. Several state-space reduction methods have been developed to tackle this problem. In this paper, we develop algorithms for combining two of these methods: state equivalence class reduction and the sweep-line. The algorithms allow deadlocks to be detected by recording terminal states of the system on-the-fly during state-space exploration. We derive expressions for the complexity of the algorithms and demonstrate their usefulness with an industrial case study. Our results show that the combined method achieves at least a six-fold reduction of the state space for interesting parameter values compared with either method used in isolation while still proving the desired system property of the terminal states. The runtime performance of the combined method is almost the same as that of the equivalence class method over the chosen parameter range. Moreover, the improvement in space reduction increases with increased parameter values.

In this paper, we present a computer tool for verification of distributed systems. As an example, we establish the correctness of Lamport's Fast Mutual Exclusion Algorithm. The tool implements the method of occurrence graphs with symmetries (OS-graphs) for Colored Petri Nets (CP-nets). The basic idea in the approach is to exploit the symmetries inherent in many distributed systems to construct a condensed state space. We demonstrate a significant increase in the number of states which can be analyzed. The paper is to a large extent self-contained and does not assume any prior knowledge of CP-nets (or any other kinds of Petri Nets) or OS-graphs. CP-nets and OS-graphs are not our invention. Our contribution is the development of the tool and verification of the example, demonstrating how the method of occurrence graphs with symmetries can be put into practice.