The data, links, and images in this file are auto-generated from HAMR's report generation facility. Additional text explanations have been added for readability.
The following documentation blocks provide links to AADL textual representation source of the Thread components in the system.
- "Type" links to the AADL component type declaration (providing the port-based interface for the component)
- "Behavior Specification" (when present) links to the GUMBO behavior contract for the component. HAMR automatically compiles the GUMBO contract to both an code-level contract used for Logika code verification as well as an executable representation of the contract (as pure boolean functions) used in unit and system testing.
| System: Isolette::isolette.single_sensor |
|---|
| Thread: HS |
|---|
| Type: Devices::Heat_Source Implementation: Devices::Heat_Source.impl |
| Periodic: 1000 ms |
| Thread: TS |
|---|
| Type: Devices::Temperature_Sensor Implementation: Devices::Temperature_Sensor.impl |
| Periodic: 1000 ms |
| Thread: OpInterface |
|---|
| Type: Isolette::operator_interface_thread Implementation: Isolette::operator_interface_thread.impl |
| Periodic: 1000 ms |
| Thread: DMF |
|---|
| Type: Monitor::Detect_Monitor_Failure Implementation: Monitor::Detect_Monitor_Failure.impl |
| Periodic: 1000 ms |
| Thread: MA |
|---|
| Type: Monitor::Manage_Alarm Implementation: Monitor::Manage_Alarm.impl Behavior Specification: GUMBO |
| Periodic: 1000 ms |
| Thread: MMI |
|---|
| Type: Monitor::Manage_Monitor_Interface Implementation: Monitor::Manage_Monitor_Interface.impl Behavior Specification: GUMBO |
| Periodic: 1000 ms |
| Thread: MMM |
|---|
| Type: Monitor::Manage_Monitor_Mode Implementation: Monitor::Manage_Monitor_Mode.impl Behavior Specification: GUMBO |
| Periodic: 1000 ms |
| Thread: DRF |
|---|
| Type: Regulate::Detect_Regulator_Failure Implementation: Regulate::Detect_Regulator_Failure.impl |
| Periodic: 1000 ms |
| Thread: MHS |
|---|
| Type: Regulate::Manage_Heat_Source Implementation: Regulate::Manage_Heat_Source.impl Behavior Specification: GUMBO |
| Periodic: 1000 ms |
| Thread: MRI |
|---|
| Type: Regulate::Manage_Regulator_Interface Implementation: Regulate::Manage_Regulator_Interface.impl Behavior Specification: GUMBO |
| Periodic: 1000 ms |
| Thread: MRM |
|---|
| Type: Regulate::Manage_Regulator_Mode Implementation: Regulate::Manage_Regulator_Mode.impl Behavior Specification: GUMBO |
| Periodic: 1000 ms |
The following items link to the Slang source code for the application logic of each thread. In the HAMR development workflow, skeletons for these files are automatically created, along with APIs for communicating over model-declared ports in the component type. GUMBO component contracts in the AADL model are automatically translated to Slang/Logika contracts and included in the generated skeletons. Then, the application developer uses a conventional development approach for coding the application logic in Slang (C workflows are also supported). Logika can be applied to verify that the user's application code conforms to the generated Logika contracts (which are derived automatically from model-level GUMBO contracts). The HAMR build framework will integrate the user-code application logic for each component (below) with auto-generated threading and communication infrastructure code, along with HAMR's implementation of AADL run-time (based on AADL's standardized Run-Time Services). Note that HAMR is smart enough to accommodate changes to model-level interface declarations (ports, etc.) as well as changes to GUMBO contracts -- user code will not be clobbered when the model is changed and HAMR code generation is rerun. Instead, HAMR uses specially designed delimiters in the application code files to, e.g., re-weave updated contracts into the application code.
Executable Slang versions of the GUMBO contracts (referred to as "GUMBOX" contracts) are also automatically generated in the code generation process. These executable contracts are automatically integrated into the unit testing process: appropriate portions of the executable contracts are invoked in the pre-state and the post-state of a thread dispatch to dynamically check that the thread's behavior for that particular dispatch conforms to the model-level GUMBO contracts.
The following section provides statistics about the AADL model to give a rough idea of its size (in terms of number of AADL modeling elements that impact the size of the deployed system).
| Threads | 11 |
| Ports | 49 |
| Connections | 27 |
The following section provides statistics about the Slang source code.
Directories Scanned Using https://github.com/AlDanial/cloc v1.94:
Total LOC
Total number of HAMR-generated and developer-written lines of code
| Language | files | blank | comment | code |
|---|---|---|---|---|
| Scala | 121 | 4483 | 2493 | 19954 |
| -------- | -------- | -------- | -------- | -------- |
| SUM: | 121 | 4483 | 2493 | 19954 |
User LOC
The number of lines of code written by the developer. "Log" are lines of code used for logging that likely would be excluded in a release build
| Type | code |
|---|---|
| Behavior | 184 |
| Log | 16 |
| -------- | -------- |
| SUM: | 200 |
-
Auto-generated GUMBOX Unit Test Harness link, that was subsequently modified to provide custom configurations
-
Auto-generated component coverage report using the configurations below link. Custom configurations were used for this component. Click here for the coverage report obtained when only the default configurations are used
-
Configurations for the Initialize Entrypoint
Default_Initialize_Config Default Initialize Configuration -
Configurations for the Compute Entrypoint
Compute_Config_ranges_based_on_requirements Ranges based on requirements - ie 96.0 <= lower_alarm <= 101.0 and 97.0 <= upper_alarm <= 102. Also restrict current_temp to be between 86.0 and 112.0 inclusive
-
-
Auto-generated GUMBOX Unit Test Harness link
-
Auto-generated component coverage report using the configurations below link
-
Configurations for the Initialize Entrypoint
Default_Initialize_Config Default Initialize Configuration -
Configurations for the Compute Entrypoint
Default_Compute_Config Default Compute Configuration Default_ComputewL_Config Default ComputewL Configuration
-
-
Auto-generated GUMBOX Unit Test Harness link
-
Auto-generated component coverage report using the configurations below link
-
Configurations for the Initialize Entrypoint
Default_Initialize_Config Default Initialize Configuration -
Configurations for the Compute Entrypoint
Default_Compute_Config Default Compute Configuration Default_ComputewL_Config Default ComputewL Configuration
-
-
Auto-generated GUMBOX Unit Test Harness link
-
Auto-generated component coverage report using the configurations below link
-
Configurations for the Initialize Entrypoint
Default_Initialize_Config Default Initialize Configuration -
Configurations for the Compute Entrypoint
Default_Compute_Config Default Compute Configuration Default_ComputewL_Config Default ComputewL Configuration
-
-
Auto-generated GUMBOX Unit Test Harness link
-
Auto-generated component coverage report using the configurations below link
-
Configurations for the Initialize Entrypoint
Default_Initialize_Config Default Initialize Configuration -
Configurations for the Compute Entrypoint
Default_Compute_Config Default Compute Configuration
-
-
Auto-generated GUMBOX Unit Test Harness link
-
Auto-generated component coverage report using the configurations below link
-
Configurations for the Initialize Entrypoint
Default_Initialize_Config Default Initialize Configuration -
Configurations for the Compute Entrypoint
Default_Compute_Config Default Compute Configuration Default_ComputewL_Config Default ComputewL Configuration
-