Merge pull request #125 from GaloisInc/121-write-the-final-report

121 write the final report

.gitmodules

@@ -1,3 +1,8 @@
 [submodule "hardware/nerv"]
 	path = hardware/nerv
 	url = https://github.com/YosysHQ/nerv.git
+[submodule "report"]
+	path = report
+	url = https://git.overleaf.com/623259a297f75c655f6d1f47
+
+

Dockerfile

@@ -1,11 +1,11 @@
 # Base
-FROM ubuntu:21.04 as base
+FROM ubuntu:22.04 as base
 ARG DEBIAN_FRONTEND=noninteractive
 RUN mkdir /tools
 WORKDIR /
 
 RUN apt-get update && apt-get upgrade -y
-RUN apt-get install -y wget git python pip \
+RUN apt-get install -y wget git python3 pip \
     python3-dev software-properties-common \
     iproute2 usbutils srecord \
     build-essential clang bison flex \
@@ -23,7 +23,8 @@ RUN apt-get install -y wget git python pip \
     libftdi1-2 libftdi1-dev libhidapi-libusb0 libhidapi-dev libudev-dev make g++ \
     libc++-dev libc++abi-dev nodejs python2 npm \
     iverilog verilator \
-    vim mercurial libboost-program-options-dev
+    vim mercurial libboost-program-options-dev \
+    texlive-full
 
 # Builder
 FROM base as builder
@@ -255,6 +256,25 @@ RUN \
 
 ENV PATH="/tools/:${PATH}"
 
+# NuSMV
+# wget https://nusmv.fbk.eu/distrib/NuSMV-2.6.0-linux64.tar.gz
+# tar xzf NuSMV-2.6.0-linux64.tar.gz
+# cp NuSMV-2.6.0-Linux/bin/* /usr/local/bin/
+
+# JKind-1
+# wget https://github.com/andreaskatis/jkind-1/releases/download/v2.0/jkind
+# wget https://github.com/andreaskatis/jkind-1/releases/download/v2.0/jkind.jar
+# wget https://github.com/andreaskatis/jkind-1/releases/download/v2.0/jlustre2kind
+# wget https://github.com/andreaskatis/jkind-1/releases/download/v2.0/jrealizability
+# chmod 755 jkind jlustre2kind jrealizability
+# cp * /usr/local/bin/
+
+# Kind 2
+# wget https://github.com/kind2-mc/kind2/releases/download/v1.6.0/kind2-v1.6.0-linux-x86_64.tar.gz
+# wget https://github.com/kind2-mc/kind2/releases/download/v1.6.0/user_documentation.pdf
+# tar xzf kind2-v1.6.0-linux-x86_64.tar.gz
+# mv kind2 /usr/local/bin/
+
 # Fret
 # ARG TOOL=fret
 # ARG TAG=7dbfbf65d8b7f96e9f1fdca2dd19a2a2387d2674
@@ -282,6 +302,17 @@ RUN cd /tools/${TOOL}/source/lobot/ && cabal v2-build
 ENV PATH="/tools/${TOOL}:${PATH}"
 RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
 
+# DocumentationEnricher
+ARG TOOL=der
+ARG TAG=0.1.4
+ARG REPO=https://github.com/SimplisticCode/DER/releases/download/v1.1.4/
+WORKDIR /tmp
+RUN wget ${REPO}/${TOOL}-${TAG}.zip
+RUN unzip ${TOOL}-${TAG}.zip
+RUN    mv ${TOOL}-${TAG} /tools/${TOOL}
+ENV PATH="/tools/${TOOL}/bin:${PATH}"
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
 # Runner
 FROM base as runner
 COPY --from=builder /opt/ /opt/
@@ -296,4 +327,4 @@ WORKDIR /HARDENS
 # Install java so we can run lando
 RUN apt-get install -y default-jre
 
-ENV PATH="/tools/lando:/tools:/tools/z3/bin:/tools/bsc-2021.07-ubuntu-20.04/bin:/opt/riscv/bin:/opt/bin:${PATH}"
+ENV PATH="/tools/der/bin:/tools/lando:/tools:/tools/z3/bin:/tools/bsc-2021.07-ubuntu-20.04/bin:/opt/riscv/bin:/opt/bin:${PATH}"

README.md

@@ -255,8 +255,8 @@ tools to this container as necessary during project execution.
 
 ### HARDENS Container
 
-To build and run the core HARDENS Docker image, use the `build_docker.sh` script and then
-`docker run` commands.
+To build and run the core HARDENS Docker image, use the
+`build_docker.sh` script and then `docker run` commands.
 
 ```
 $ ./build_docker.sh
@@ -271,6 +271,14 @@ directory in order to bind your sandbox properly into the container.
 $ docker run -d -it --name HARDENS --network host --privileged -v $PWD:/HARDENS hardens:latest
 ```
 
+If you have stopped a container running and it lists as "exited" when
+you run a `docker container ls`, then you can restart it with the
+following command.
+
+```
+$ docker start HARDENS
+```
+
 After running such a detacted container, attach to it for interactive
 use by running a command like:
 ```
@@ -284,6 +292,8 @@ $ docker pull artifactory.galois.com:5015/hardens:latest
 $ docker run --network host --privileged -v $PWD:/HARDENS -it artifactory.galois.com:5015/hardens:latest
 ```
 
+The helper script `run_docker.sh` executed the above detacted run
+command, using Galois's `artifactory` docker image name.
 
 ### SysMLv2 Container
 
@@ -296,6 +306,19 @@ $ docker pull gorenje/sysmlv2-jupyter:latest
 $ docker run -d -it --name SysMLv2 --network host -v $PWD:/HARDENS gorenje/sysmlv2-jupyter:latest
 ```
 
+The Docker container contains snapshots of various tools that are not
+necessarily the latest releases or development versions of said tools.
+We include these particular versions because they are the versions
+used for development of the demonstrator, in alignment with our
+*Tool Dependencies* recommendations, **Tool Metadata**, **Tool
+Availability**, and **Evaluation Platform**.
+
+In particular, the version of Lando shipped in the image is incapable
+of converting Lando input files into hyperlinked Markdown, as we
+provide in [specs/Lando/](specs/Lando/).  This is partly due to the
+fact that the new version of Lando is not ready for release and is
+only available via Galois's private GitLab server.
+
 ## Lattice ECP5 evaluation board
 
 We are using an ECP5-5G FPGA board for the RTS demonstrator.
@@ -345,32 +368,56 @@ and tools of model-driven engineering in the large.  This means that
 we will be reviewing technologies that are used in the project as well
 as those that are commonly used for MDE for hardware, firmware,
 software, systems, safety, and security engineering.  Tools reviewed
-will include 
+will include all mainstream MBSE tools, tools that we use for
+demonstrating correct-by-construction components and subsystems, and a
+variety of assurance tools.
+
+There are three versions of the HARDENS talk:
+ 1. A [short version summarizing the HARDENS
+    project](docs/HARDENS_HCSS_May_2022.pdf), which was given at HCSS
+    in May 2022.
+ 2. A [90 minute
+    version](docs/HARDENS_Galois_Explaining_RDE_by_Example_May_2022.pdf)
+    which was used to give a presentation at Galois in May 2022 about
+    Rigorous Digital Engienering.  Friends of Galois attended this
+    talk as well.
+ 3. A [six hour version that was the final presentation for the entire
+    project to the NRC](docs/HARDENS_NRC_Oct_2022.pdf), given on 12
+    October 2022.
+
+These presentations were all written using Apple Keynote.  The
+canonical source for the final presentation is found in the file
+[HARDENS.key](docs/HARDENS.key).  A Powerpoint version of the slide
+deck is also exported from Keynote and in the same directory. No
+attempt has been made to make sure the exported Powerpoint is pretty.
 
 ## Final Report
 
 Our final report for HARDENS must have the following characteristics:
- 1. [ ] it must be well-suited to fit into the document-centric
+ 1. [X] it must be well-suited to fit into the document-centric
         certification process used by the NRC and other similar
         government agencies,
- 2. [ ] it must completely describe the framing for the project, the
+ 2. [X] it must completely describe the framing for the project, the
         technical work, the safety and correctness assurance case of
         the RTS demonstrator, and the manner in which the document can
         be read, the R&D can/should be reviewed, etc.
- 3. [ ] It must include all formal specifications and assurance
+ 3. [X] It must include all formal specifications and assurance
         artifacts as nicely typeset, hyper-textual cross-referenced
         appendix chapters.
 
 In order to fulfill (1) above, the final report must be both:
- 1. [ ] a polished, high-quality, hyperlinked HTML webpage, or set of
+ 1. [X] a polished, high-quality, hyperlinked HTML webpage, or set of
         webpages that compile into a single webpage, that contains the
         entire report, includes its technical appendices, and
- 2. [ ] a polished, high-quality, hyperlinked PDF document that can be
+ 2. [X] a polished, high-quality, hyperlinked PDF document that can be
         printed on paper and, in that form, it just as easy to read
         front-to-back and to follow cross-references therein.
 
 In order to help certification actors review a model-based system and
 its assurance case, we intend to provide a chapter in the report that
 characterizes a workflow and set of best practices for such a review.
 
-The final report is available in overleaf: https://git.overleaf.com/623259a297f75c655f6d1f47
+The final report is available [via
+Overleaf](https://git.overleaf.com/623259a297f75c655f6d1f47) as well
+as a submodule on this project.
+

compileLatexFiles.sh

@@ -0,0 +1,2 @@
+#! /usr/bin/env bash
+der -i /HARDENS -o /HARDENS/output -e /HARDENS/cryptol-codegen,/HARDENS/cryptol-verilog -g