5 ms·

Most of my career has been as a "software engineer" in aerospace. We absolutely do build things to requirements, and verify those requirements are met, with cop

by tjr 6y ago

Most of my career has been as a "software engineer" in aerospace. We absolutely do build things to requirements, and verify those requirements are met, with copious amounts of formal process. This same style of development could be applied to any software development venture, but it's usually not, because most software doesn't benefit from it enough to warrant the extra time and expense.

kaba0 6y ago
May I ask you what sort of tools you use for verification, including language? Is it model checkers like TLA+?
- tjr 6y ago
  If you are asking me personally, my verification experience has been a mixture of manual tests, and writing test scripts in either Python or a custom in-house language. These scripts run in an avionics simulation environment, in which typically there is one avionics component under test, which is running either a desktop build of its code, or running as the actual hardware unit, attached to a desktop via Ethernet or ARINC 429 connections. The other avionics components are then either simulated, or, as needed, running actual code. (The majority of my avionics work has actually been directly working on such simulation systems, building and certifying them for formal verification use, but I have done some verification work on avionics boxes as well.) Outside of my personal experience, I am aware of projects using things like TLA+. I suspect that is more common the higher up you go in system criticality. Even within avionics, not every system requires the same level of scrutiny... for example, you need to more exhaustively test a flight controls system than a flight management system. In any case, the FAA does not dictate particular tools. They dictate a level of quality that any tools used must adhere to (the tools themselves must be certified based on how they are used), but otherwise a project is welcome to use whatever tools they wish. Or, no tools.
analog31 6y ago
Amusingly, the engineers I work with have a saying, which is: "This is not aerospace," meaning that they will not apply formal engineering methods in their design processes.

by tjr 6y ago

kaba0 6y ago

May I ask you what sort of tools you use for verification, including language? Is it model checkers like TLA+?

tjr 6y ago
If you are asking me personally, my verification experience has been a mixture of manual tests, and writing test scripts in either Python or a custom in-house language. These scripts run in an avionics simulation environment, in which typically there is one avionics component under test, which is running either a desktop build of its code, or running as the actual hardware unit, attached to a desktop via Ethernet or ARINC 429 connections. The other avionics components are then either simulated, or, as needed, running actual code. (The majority of my avionics work has actually been directly working on such simulation systems, building and certifying them for formal verification use, but I have done some verification work on avionics boxes as well.) Outside of my personal experience, I am aware of projects using things like TLA+. I suspect that is more common the higher up you go in system criticality. Even within avionics, not every system requires the same level of scrutiny... for example, you need to more exhaustively test a flight controls system than a flight management system. In any case, the FAA does not dictate particular tools. They dictate a level of quality that any tools used must adhere to (the tools themselves must be certified based on how they are used), but otherwise a project is welcome to use whatever tools they wish. Or, no tools.

analog31 6y ago

Amusingly, the engineers I work with have a saying, which is: "This is not aerospace," meaning that they will not apply formal engineering methods in their design processes.