In an era of sequestration and austerity, the federal government is seeking software reuse strategies that will allow them to move away from stove-piped development toward open, reusable architectures. The government is also motivated to explore reusable architectures for purposes beyond fiscal constraints: to leverage existing technology, curtail wasted effort, and increase capabilities rather than reinventing them. An open architecture in a software system adopts open standards that support a modular, loosely coupled, and highly cohesive system structure that includes the publication of key interfaces within the system and full design disclosure.
When we verify a software program, we increase our confidence in its trustworthiness. We can be confident that the program will behave as it should and meet the requirements it was designed to fulfill. Verification is an ongoing process because software continuously undergoes change. While software is being created, developers upgrade and patch it, add new features, and fix known bugs. When software is being compiled, it evolves from program language statements to executable code. Even during runtime, software is transformed by just-in-time compilation. Following every such transformation, we need assurance that the change has not altered program behavior in some unintended way and that important correctness and security properties are preserved. The need to re-verify a program after every change presents a major challenge to practitioners--one that is central to our research. This blog post describes solutions that we are exploring to address that challenge and to raise the level of trust that verification provides.
With the rise of multi-core processors, concurrency has become increasingly common. The broader use of concurrency, however, has been accompanied by new challenges for programmers, who struggle to avoid race conditions and other concurrent memory access hazards when writing multi-threaded programs. The problem with concurrency is that many programmers have been trained to think sequentially, so when multiple threads execute concurrently, they struggle to visualize those threads executing in parallel. When two threads attempt to access the same unprotected region of memory concurrently (one reading, one writing) logical inconsistencies can arise in the program, which can yield security concerns that are hard to detect.
Given that up to 70 percent of system errors are introduced during the design phase, stakeholders need a modeling language that will ensure both requirements enforcement during the development process and the correct implementation of these requirements. Previous work demonstrates that using the Architecture Analysis & Design Language (AADL) early in the development process not only helps detect design errors before implementation, but also supports implementation efforts and produces high-quality code. Our latest blog posts and a recent webinarhave shown how AADL can identify potential design errors and avoid propagating them through the development process. Verified specifications, however, are still implemented manually.