Abstract
With the increasing importance of software in the aerospace field, as evidenced by its growing size and complexity, a rigorous and reliable software verification and validation process must be applied to ensure conformance with the strict requirements of this software. Although important, traditional validation activities such as testing and simulation can only provide a partial verification of behavior in critical real-time software systems, and thus, formal verification is an alternative to complement these activities. Two useful formal software verification approaches are deductive verification and abstract interpretation, which analyze programs statically to identify defects. This paper explores abstract interpretation and deductive verification by employing Frama-C's value analysis and Jessie plug-ins to verify embedded aerospace control software. The results indicate that both approaches can be employed in a software verification process to make software more reliable.

Abstract

Abstract
Pure operation-based (op-based) Conflict-free Replicated Data Types (CRDTs) are generic and very efficient as they allow for compact solutions in both sent messages and state size. Although the pure op-based model looks promising, it is still not fully understood in terms of practical implementation. In this paper, we explain the challenges faced in implementing pure op-based CRDTs in a real system: the well-known in-memory cache key-value store Redis. Our purpose of choosing Redis is to implement a multi-master replication feature, which the current system lacks. The experience demonstrates that pure op-based CRDTs can be implemented in existing systems with minor changes in the original API. © 2016 Copyright held by the owner/author(s).

Abstract
State-based CRDTs allow updates on local replicas without remote synchronization. Once these updates are propagated, possible conflicts are resolved deterministically across all replicas. d-CRDTs bring significant advantages in terms of the size of messages exchanged between replicas during normal operation. However, when a replica joins the system after a network partition, it needs to receive the updates it missed and propagate the ones performed locally. Current systems solve this by exchanging the full state bidirectionally or by storing additional metadata along the CRDT. We introduce the concept of join-decomposition for state-based CRDTs, a technique orthogonal and complementary to delta-mutation, and propose two synchronization methods that reduce the amount of information exchanged, with no need to modify current CRDT definitions. © 2016 Copyright held by the owner/author(s).

Abstract
Any computing system can be described as executing sequences of actions, with an action being any relevant change in the state of the system. For example, reading a file to memory, modifying the contents of the file in memory, or writing the new contents to the file are relevant actions for a text editor. In a distributed system, actions execute in multiple locations; in this context, actions are often called events. Examples of events in distributed systems include sending or receiving messages, or changing some state in a node. Not all events are related, but some events can cause and influence how other, later events occur. For example, a reply to a received mail message is influenced by that message, and maybe by prior messages received.

Abstract
Edge/Fog Computing is an extension to the Cloud Computing model, primarily proposed to pull some of the load on cloud data center towards the edge of the network, i.e., closer to the clients. Despite being a promising model, the foundations to adopt and fully exploit the edge model are yet to be clear, and thus new ideas are continuously advocated. In his paper on \Life beyond Distributed Transactions: An Apostate's Opinion", Pat Helland proposed his vision to build\almost innite" scale future applications, demonstrating why Distributed Transactions are not very practical under scale. His approach models the applications data state as independent \entities" with separate serialization scopes, thus allowing ecient local transactions within an entity, but precluding transactions involving dierent entities. Accessing remote data (which is assumed rare) can be done through separate channels in a more message-oriented manner. In this paper, we recall Helland's vision in the aforementioned paper, explaining how his model ts the Edge Computing Model either regarding scalability, applications, or assumptions, and discussing the potential challenges leveraged . © 2016 ACM.