christofferholmstedt / dva501-master-thesis-report Goto Github PK

Background

A manager of a VN network must be able to monitor the network. This means that the manager must be able to view the current status of all application nodes and LS, CAS as well as all Gateways.

How to demo

The user launch the monitoring GUI and is presented with a list of all networks/CAS nodes available (A monitoring application can be connected to multiple VN networks). The user selects one and get a list of all nodes available on that network with respective node's capabilities which is automatically requested in the background from LS.

The user can now select one node for further information from the list of nodes.

Without streams and other high-level language features how does high-integrity systems do IO?

Background

Large apartment buildings usually suffers from indoor temperature fluctuations when the temperature outside rapidly changes, the heating of large buildings is a slow system.

How to demo

The user add one temperature sensor per room and one or more outside, that connects to the sensor network and starts reporting information to a central monitoring (web?) service.

The monitoring service should show how the outdoor temperature relates to the different indoor temperatures in different graphs.

UPPAAL / Modeling / Formal methods

???

Ada programming (incl. tasks)

A couple of whitepapers from AdaCore, need journals/article from Academia.
"Guide for the Use of the Ada Programming Language in High Integrity Systems"
"Guide for the use of the Ada Ravenscar Profile in high integrity systems"
"High-Integrity Object-Oriented Programming in Ada"
"Ada 2012 Rationale"

SPA

SPA Standard at AIAA (no access from Mälardalen University)
SYSTEM DATA MODEL (SDM) SOURCE CODE with references released as public domain from dtic.mil, available at https://github.com/virtual-network/vn-sdm/blob/master/release_documentation/SDM%20Release%20Report%20AFRL-RV-PS-TP-2012-0062.pdf

High Integrity

First defining what "high integrity" means.
"Basic Concepts and Taxonomy of Dependable and Secure Computing"
"From Dependability to Resilience"

Internet of Things / Home Automation

CoAP, application layer
DNS-SD (DNS Service Discovery)
Samsung Software Protocol
AllSeen/AllJoyn by Qualcomm now run by Linux Foundation

6LoWPAN
Bluetooth LE (low energy) / Bluetooth SMART (marketing term), Bluetooth 4.1 from december 2013

A comparison? How do I analyse an event triggered system?

The conclusion states: "Presented in this thesis report is a model-checked implementation of ...", but there is in fact very little presentation of the implementation in the report. Appendix A gives a very high level picture of the components (but the appendix is not references or mentioned in the main sections), but that is not enough to get a good understanding of the implementation, and thus it is hard to judge if the presented time automata models are correct or not.

The conclusion (second paragraph) says that the model checking proves that the implementation behaves according to the SPA standards, but from the description in the report it seems only focused on deadlock- and livelock freeness.

The introduction says that Uppaal will be used to verify realtime requirements, but it seems it is only used for deadlock and livelock analysis, not any verification of timing.

Read up on the Safety and Security annex in the Ada standard.

Blandning av gemener och versaler. T.ex. "uppaal/pnpsat/…". Använd { } i bibtex för att fixa detta. T.ex. title={…language of {SPA}}
Ref nummer 36 är inte komplett.

Uppaal och SPA är bra beskrivet, men det saknas en jämförelse mellan Ditt arbete och andras arbete.

This is the goal for my thesis and will make it possible to have other applications running on the same processing node.

For the literature study described in 3.1 it is not clear what the goal of it was (was it to answer some specific questions or just to form a general understanding of the field?

Virtual Network Protocol (VNP) is a working title. We need to settle for a name when moving from SPA to this new middleware written in Ada.

Should we keep the name Virtual Network Protocol (VNP)?

Requirements

Ada Tasks (Ravenscar)
Tagged Types (Object-Oriented Programming)

What should not be required

Controlled Types (requires a lot from the run-time system)

Which license should be used for the code?

We're using the GCC compiler so I assume that puts some restrictions on which licenses we can choose from.

After conducting the literature study a research question must be stated.

More importantly, it is also not clear what the results of the literature study were.

The overall problem addressed in the thesis is clear (How to correctly implement parts of SPA using Ada). However, it is not clear what the main challenges in doing this are, and how were these challenges solved?

When the list of context, figures, tables or abbrevations grows longer than one page the header and footer on the following pages are wrong, this must be fixed.

What's the effect of using zero footprint profiles or the Ravenscar profile on object code size? What is kind of reduction in object code size is expected?

Instead go to

Inkludera fler bilder i introduktionen. Architectural concepts ter sig svåra att förstå via enbart text.

When the research question is stated a method must be chosen. Which are suitable for this thesis work and which one should I choose?

It is not possible to write GUI programs and validate them with formal methods as of now. How do you properly create a GUI that interacts with a high-integrity system in the background that is verified with formal methods?

Unclear what the reader should get from figures 6.1-6.3.

http://www.adaic.org/resources/add_content/standards/95lrm/ARM_HTML/RM-D.html

Read up on "Discriminants in Ada".

The choice of verification and validation method(s) will impact the design choices made and influence which parts of the Ada language that can be used.

I detected some minor spelling mistakes and typos. For instance:

Abstract: "this thesis present"
Page 6: "it's" and "scheduability"
Page 31: "neglectable" (negligible?) and "This among other things lead to" ('lead' should be either leads or led).

An extra check with a speller can be useful.

I found this paragraph in the Conclusion (page 33) difficult to understand:
(...) quite a lot of discussions went into which level of safety that was expected, as there were no specific application in mind there was no way to decide which techniques that were going to be used to test the system in the end. Instead time went into discussing which Ada features that were thought to be useful and which ones should be avoided.

A lot of the references within the SPA community goes to AIAA. Access to AIAA journals is not given through MDH.

Some language issues (e.g. "As a part of SPA is the ...", the first sentence of the abstract which should be two sentences or rewritten, "appopiate" on page 23, "The livelock query make sure").

Also, the title seems a bit odd to me (why a comma after "model-checked" and "Space Plug-and-Play Architecturs Local Subnet Adaptation" sounds strange but that's maybe just because the domain is new to me).

Maybe this is a good start http://www.seas.gwu.edu/~adagroup/sigada-website/barnes-html/chap3.html

The master thesis report should include the following chapters:

**First chapters**
1. Abstract
2. Acknowledgement
3. Table of Contents
4. List of Figures
5. List of Tables
6. List of Abbreviations

**Main chapters**
1. Introduction
  1. Background (including move to VN, and proof-of-concept with IoT)
  2. Problem statement
2. State of the Art
  1. Space plug-and-play Avionics
  2. Ada and Dependability
  3. Model Checking and UPPAAL
  4. Internet of Things
3. Method
  1. Literature study
  2. Requirements analysis
  3. Design with UML
  4. Modeling, validation and verification with UPPAAL
  5. Development in Ada
  6. Iteration of 3.2 to 3.5 twice during the thesis work
4. Result
5. Conclusion

**Last chapters**
1. Bibliography
2. Appendices

The master thesis report should include the following sections and subsections:

What is in scope for my research question?
What is not in scope for my research question?

References to "lecture notes"?

GNATcheck can be used to verify coding guidelines but should GNAT specific tools be used at all?