LoRa is a low power, long range modulation scheme that has grown in popularity in recent years. Wireless sensors utilizing LoRa have very limited bandwidth, particularly in regions like the EU, that impose strict 1% duty cycles. Thus, it is critical to reduce the number of transmissions while still meeting performance goals. In doing so, these sensors can greatly improve the quality of service and extend the battery life of the sensors. The importance of efficient bandwidth usage is amplified in time critical applications, such as in feedback control. In this work, we studied event-based transmission schemes used for sampling the state of a control system. Modern communication protocols, such as LoRa, have different transmission options to match transmission rates to channel quality. To model these transmission options, we extended past work by modeling the option to use different transmission schemes, which have independent packet drop rates and quantization error. To this end, we developed model based algorithms to allow nodes to adapt to unknown channel conditions when transmitting packets. We verified the performance of these algorithms in simulation and compared them to previous work.

Low power, long range wireless sensor networks (WSMs) have found many applications, but are often limited to small packets and low data rates. To improve data throughput, lossy compression can be utilized. This however, induces distortion in the data which can harm the accuracy of the underlying applications. This can be especially dangerous in safety critical applications, where incorrect classifications can cause serious harm, but a lack of new updates can be just as dangerous. In this paper, we provided an example application, nodes transmitting images to a back-end classifier. The effects of distortion on classification accuracy were studied, and different metrics were examined to better predict the usefulness of the data transmitted. These metrics were used to develop models to predict the VoI for a given compression ratio (CR). With these models, we developed a reward function to provide a trade-off between timeliness of data and the precision of the data. We used this to develop algorithms which can adjust to changing channel conditions to provide the most useful information possible, in a range of network traffic conditions. In this way, data quality can degrade gently as channel traffic increases. This provided more value to back-end nodes than with other methods tested.

Summary We present a formal framework for reasoning about security concerns in the context of embedded sensor networks. We first provide an agent‐based programming model for sensor networks. A logical framework enables reasoning about security, safety, and integrity with respect to usage of resources in this model. Embedded sensor networks often operate in rapidly changing mission‐critical environments where both functional and nonfunctional requirements can alter dynamically in an unforeseen manner. The network may need to be reconfigured and reprogrammed in response to changes in its operating conditions. We provide a framework based on counterfactual logic to formally represent changes to the system and perform what‐if reasoning about their impact on security and safety even before they have been applied. Copyright © 2015 John Wiley & Sons, Ltd.

In this short paper, we provide the background to counterfactual logic and give very general suggestions on how we could employ this logic to help us reason about security policies. It seems very appropriate to use this kind of logic to anticipate a change that will compromise the security concerns of a given system before actually applying the changes.

In this paper, we present a formal framework for developing distributed service-oriented systems in an event-driven secure synchronous programming environment. More precisely, we present a synchronous programming language called SOL (Secure Operations Language) that has (i) capabilities for handling service invocations asynchronously, (ii) strong typing to ensure enforcement of information flow and security policies, and (iii) the ability to deal with failures (both benign and byzantine) of components. SOL is supported by formal operational semantics. Applications written in our framework can be verified using formal static checking techniques like theorem proving. The framework runs on the top of the SINS (secure infrastructure for networked systems) infrastructure that we have developed.

Based on our recent experience in four projects, each focused on either security-critical or safety-critical software, this paper evaluates several notions, widely held by RE researchers, for their utility in practical software development. It describes four notions which in our view work in practice and five others which do not.

The goal of the NRL secure middleware project (SINS) is to develop infrastructure for the deployment and protection of time- and mission-critical applications on a distributed computing platform, in a hostile computing environment such as the Internet, while using unreliable or untrusted COTS components. In this project, we are rethinking basic ways in which distributed applications are developed, deployed, configured, and maintained. Such a methodology and infrastructure are crucial for the deployment of mission-critical applications in a collaborative environment spanning multiple sites, by multiple agencies, and across multiple enterprises.

Building robust, secure distributed systems in the presence of transient faults, node failures, and changes in network topology poses a multitude of challenges. To meet current engineering challenges such as pervasive and ubiquitous computing, one must adopt model-driven approaches to build distributed applications. We propose the synchronous paradigm for component integration and coordination: developers use an abstraction that respects the synchrony hypothesis, i.e., each external event is processed by the system completely before the arrival of the next event. Based on the synchronous model, the Secure Operations Language (SOL) is designed as a verifiable language for the integration of high assurance systems.

Exposing inconsistencies can uncover many defects in software specifications. One approach to exposing inconsistencies analyzes two redundant specifications, one operational and the other property-based, and reports discrepancies. This paper describes a "practical" formal method, based on this approach and the SCR (software cost reduction) tabular notation, that can expose inconsistencies in software requirements specifications. Because users of the method do not need advanced mathematical training or theorem-proving skills, most software developers should be able to apply the method without extraordinary effort. This paper also describes an application of the method which exposed a safety violation in the contractor-produced software requirements specification of a sizable, safety-critical control system. Because the enormous state space of specifications of practical software usually renders direct analysis impractical, a common approach is to apply abstraction to the specification. To reduce the state space of the control system specification, two "pushbutton" abstraction methods were applied, one which automatically removes irrelevant variables and a second which replaces the large, possibly infinite, type sets of certain variables with smaller type sets. Analyzing the reduced specification with the model checker Spin uncovered a possible safety violation. Simulation demonstrated that the safety violation was not spurious but an actual defect in the original specification.