|
Research Challenges in High Confidence Systems
HCS Solution Exploration - Panelist Views |
 
|
|
|
|
|||
 |
|
|---|---|
|
|
|
|
|
Overview
|
On day two of the workshop the participants moved from problem exploration to solution exploration, suggesting and discussing the following solutions for the yet to be identified HCS challenges:
|
|
|
|
|
Software Safety and Improved Specification Tools
|
One possibility for HCS development is to pursue systems development in a manner analogous to what Nancy Leveson, a professor at the Department of Computer Science and Engineering at the University of Washington, Seattle, describes in her book, Safeware: System Safety, and Computers.17 Using the concepts of software safety and continuing research along those lines would contribute towards developing improved specifications and an integrated methodology for high confidence. Leveson has looked at many design-for-safety issues, e.g., experiments with n-version programming, experimentation with self-checks, comparative evaluation of alternative methods (fault elimination and fault tolerance), provably correct code generation, design of safe human-computer interfaces (HCI), design analysis, verification, and software fault tree analysis. She has evaluated these methods on real systems using prototype tools. Leveson is using what she terms "software deviation analysis" to see what combination of events can lead to hazardous outputs. This approach enables a better understanding of what is needed for safety-related robustness. It is an adaptation of hazardous operations (HazOp) analysis from chemical plant applications. The approach considers software requirements completeness and safety analysis. In addition, Leveson has developed RMSL, a requirements modeling and specification language. The language is essentially state charts embedded in stylized English. The goals of RMSL are to provide guidance in building specifications; completeness is enforced in the language. The language could also be model-checked for some criteria. Other goals of RMSL are the elimination of error-prone system features and improved specification readability. RMSL is being designed for a specific type of application, namely, process control models, so the language is domain specific. The foundation of design-for-safety is the structuring of specifications based on human problem solving, cognitive psychology, and systems theory. Leveson wants to produce "human-centered specifications," i.e., specifications that incorporate a focus on the human in the loop of system control. She is attempting to add "intent" into the specification to amplify the "why" component of design rationale. This will be an integration of systems and software specifications including the HCI, procedures, and physical components. The specifications will provide for traceability to better enable system evolution and re-analysis for required changes. The language will also integrate with system hazard analyses, e.g., fault tree analysis. RMSL was used to specify TCAS-II, the FAA's aircraft collision avoidance system. This work included the development of forty-seven criteria for completeness of specifications (see details in her book). Matts Heimdahl developed a "D-completeness" (mathematical completeness) and consistency analysis for two of the forty-seven criteria. The approach enables backward and forward executions of specifications to identify events leading to hazardous states. Leveson is continuing work on RMSL extensions including timing, integration of human procedure models, and mode-confusion software analysis (i.e., where the human is confused about which mode the system is in). For example, ongoing work includes analysis for restarting real-time systems. A number of accidents have been attributed to real-time software that has been taken off-line and then returned to service without synchronizing the software's internal state with the system's current state. RMSL now requires any restart to begin in an "unknown" state. Ongoing work also focuses on the integration of HCI and system operating procedures in RMSL to address the problem of operators not understanding the state of the system and, therefore, expecting different behavior. A number of accidents (including Airbus A320 problems) have been attributed to this problem. Future RMSL work will include specification-based test generation to ensure completeness of test coverage, specification-based code generation and integration with autocode systems, further extensions to HCI designs and human-computer architectures, and work on organizational safety factors. An area of investigation is the application of safety techniques to security. |
|
|
|
|
Formal Methods (1)
|
Connie Heitmeyer asserted that continued work in formal methods was an essential solution to high confidence systems. Her work at the Naval Research Laboratory (NRL) continues earlier efforts in improving systems specifications. She is using static analysis techniques to identify unused inputs and spontaneous outputs in system specifications. She is also building tools to analyze and help cope with incomplete specifications. Heitmeyer is extending David Parnas's software cost reduction (SCR) method of requirements analysis. She has developed a formal semantics to support this method and is building tool support for the more tedious, error-prone portions of specification analysis. Heitmeyer is focusing on automatic detection of errors, with executable specifications, and detailed feedback when an error occurs. She has a combination of lightweight and heavyweight tools, so that she can match the tool to the problem, using the simplest and lightest-weight tool possible. The formal semantics are state based: the system is modeled as a state machine. These semantics also enable formal modeling of the system environment, much of which is naturally continuous. The project goal is to support reasoning about various classes of properties (security, safety, reliability, real time, etc.). Her tools include a specification editor, a dependency graph browser, a consistency checker, a simulator, and verification tools. There are also tools to automatically simplify the state machine so that it can be model checked. Heitmeyer outlined where additional research is needed. One area is a sound foundation for model checking. The models currently used are almost always ad hoc and are a frequent source of errors. Needed is the capability to automatically derive the abstract models to be analyzed, and their derivation should be based on the property one is trying to prove. Then one would have a mapping from the state space of the abstract machine to the state space of the original machine. The reasoning about the abstract machine should be equivalent to the reasoning about the original machine, so that counterexamples in the abstract machine correspond to counterexamples in the original machine. This specification set should be the same set that the system engineers are working from, rather than a separate (disconnected) parallel formal process. Theorem proving will be required to show completeness and soundness. A second research issue is automatic invariant generation. Needed are sound algorithms that generate invariants from specifications. Such invariants are extremely useful in reasoning about specifications; they are useful as auxiliary invariants in proving more general system invariants, and useful in themselves as system properties. Examples are Zohar Manna's localized invariants, and the mode invariants of SCR specifications. Another research area is the formal representation of the system/software environment. This is usually ignored by model checkers. The environment should be modeled as nondeterministic and continuous. There is also a need for applied research, for example, better engineered model checkers. Counterexamples can be hundreds of states long and difficult to analyze, often cryptic to anyone not intimately familiar with the model. And it is difficult to map this back to the original specification. Errors are made in going from the concrete machine to the abstract model. We should simulate the model where model checking is too computationally expensive. Better engineered model checkers will provide automatic translation of specifications into the language of the model checker as well as easily understood feedback when an error is detected (for example, run the produced trace through a simulator). Another research area is more efficient, well-integrated decision procedures. Specifications of high confidence systems usually include variables of varied types. The formulas analyzed in such specifications can include propositional tautologies, Presburger arithmetic, linear arithmetic, etc. We will want to use all these at once. We need comparisons of different analysis techniques; comparing model checkers, for example. But we must be cautious about comparing apples and oranges because some model checkers are better for some problems than for others. Such comparisons would allow us to give guidance to system developers. (e.g., some are good for protocols, some for hardware). Trustworthy code is a requirement of high confidence systems. We need specialized models and tools for specialized domains. We should generate code from specifications and produce automatic test cases. We need to develop theorem proving systems for specialized domains. Once the user develops the overall proof strategy, the system could suggest needed lemmas and complete the trivial proof parts automatically. |
|
|
|
|
Formal Methods (2)
|
Ricky Butler discussed NASA's concern with identifying missing areas of HCS research. NASA uses formal methods to reduce errors in aviation systems. However, a mission-oriented agency such as NASA has difficulty getting basic research funding for fundamental computer science investments. Instead, NASA funded several projects to pair a formal methods team and industry partner to transition the technology. NASA has also leveraged DARPA investments as well as those by other parts of the Government. This same focus on applied research is seen in ohter Government agencies -- thus running the risk of neglecting the fundamental research essential to achieving high confidence systems. Fundamental research is needed in theorem proving technology (e.g., automated reasoning). NASA wants DARPA to fund this research. There is a spectrum of needs for verification tools, ranging from domain specific to general purpose, and from mathematician friendly to engineer friendly. NASA wants improved automated reasoning, with algorithms underneath (transparent to the user) that decide chunks of mathematics for the user. There are dozens of these formal methods tools and they all exploit the fundamental techniques developed more than a decade ago: decision procedures, term rewriting, model checking, resolution. We have no research programs aimed at advancing this technology. What challenge problems could, as a side effect, lead to funding of some of this fundamental research? One challenge problem may be to produce a next generation verification environment providing a seamless integration of different tools and strategies that are effective for different parts of the life cycle. Such an environment could support a wide variety of applications, result in a hundred-fold improvement in user productivity, provide interoperable libraries for fundamental concepts of computer science and discrete mathematics, and enable effective modeling techniques. Recent research funded by NASA has focused on requirements analysis tools and requirements specifications. This is probably because we have been trying to get industry to use these things. This is a good approach (i.e., finding errors), but we have completely neglected the refinement of requirements into executable code. If we want safe systems, then we need design verification, code verification, and certifiable and qualifiable program synthesis. We want to be able to assert that there are no safety-related errors in the system. We do not want to use formal methods just to find bugs, but to give us confidence that the product is safe. Existing code synthesis has not been designed with certifiability in mind. We need new ideas on how to advance automated deduction. We need research to identify parts of arithmetic we can reason about (e.g., a theory of bit vectors), and we need decision procedures for modular arithmetic. We could use more tools to exploit graph theory and other aspects of mathematics. We also need to identify new relevant domains and the limitations in the current formal methods tools. There will continue to be a trade-off between funding new fundamental research and transitioning newly developed technology into engineering practice. The concern is how scarce resources should be best focused. One barrier to use of current formal methods technology is the sheer horsepower needed to do the analysis. However, the situation has greatly improved in the past several years. Rather than looking at the past attempts and costs of formal methods application, we need a significant, visible demonstration of what can be done today. At the same time, we must be cautious in our claims. We need to calibrate some of the differences between what was and what is now. For example, the time to produce a mathematics book was about five years in 1960; today we could use SRI International's PVS verification system to produce that same book within a few months. Can we further quantify the changes in how long it takes to do a particular verification? There could be a quantum improvement demonstrated simply because computers have gotten faster and more capable by a larger factor. |
|
|
|
|
Formal Methods (3)
|
John Rushby of SRI International asserted several research challenges for formal methods. These extend from refutation (debugging) to verification (assurance). We need to abstract rather than to downscale, as Heitmeyer said, and the abstractions must be mechanized. In the past, researchers didn't have the horsepower to do this, but with today's tools they can do it. We need a repertoire of mechanized deduction methods, not just model checking, to construct, justify, and use these abstractions. Today's model checking's simplification of problems is too crude, the simplified system models used as input are arbitrarily downscaled, and we can't provide assurance that nothing is wrong with the real system as opposed to the system model that may, for example, have fewer and shorter buffers than the real system. We need justifiable simplifications/abstractions. Heitmeyer's abstraction methods are good, and we need still other abstraction techniques. This will make it possible to address large problems. Much of the work in automated deduction in the near future will be in using computation to simplify the theorems that must be proven. Rushby suggested composing locally checked designs and properties. For example, one might model check small fragments and glue these together in some way. A combination of model checking and theorem proving is possible, but it raises issues such as language issues. Formal methods research that is being applied to hardware now must focus on systems issues that are at least seven years out from now. Requiring verification systems to hook up to the Very High Speed Integrated Circuit (VHSIC) Hardware Design Language (VHDL), for example, shackles us to the transient present. Rushby believes that Intel has a better vision for this research than the research funding agencies. Not only do we need to develop suitable methods, we need to integrate algorithmic and interactive methods. We need to integrate formal methods with testing and safety analysis techniques such as fault tree analysis and reachability analysis. One goal for formal methods is to be able to provide a calculation of properties of models. This should be done as part of the engineering process in a fashion similar to computational fluid dynamics except the calculation is done by mechanized deduction (model checking, decision procedures, interactive theorem proving). The ability for model checking to find bugs in complex systems has been adequately demonstrated and has led to widespread acceptance in certain fields including hardware and protocols. It has successfully helped hardware engineers avert many bugs in processor and cache designs. Model checking is being exploited to find problems in protocols (communication, authentication), distributed algorithms, chemical and nuclear engineering control systems, and fault-management in spacecraft. Its application to additional problem domains should be pursued. We have witnessed a tremendous increase in capabilities over the last ten years, and we can foresee tremendous opportunities in next ten. The kind of systems people are building is changing rapidly and drastically in a way that is inimical to providing any guarantees, so we could provide major enablers for what people want to do. We need to use formal methods to dispense with what is trivially computable, and allow the human to focus attention on discovering other problems. Rushby believes that we must focus research more on paradigmatic examples than on big industrial problems; it is this approach that will help avoid our overselling formal methods. |
|
|
|
|
Lowering the Cost of Entry
|
Higher-Confidence Systems from Low-Confidence Parts Ed Felton from Princeton University asserted that we need to lower the cost of entry in achieving higher confidence systems. He believes there are several key ingredients to making this happen: education, technology transfer, intuitive means of increasing confidence, and empirically based "economic coping." The biggest impediment to building system with high confidence is that people in the field (i.e., programmers) do not see the usefulness of thinking carefully and systematically about the code they write. We need to address this in education early on by teaching respect for addressing a coding task more formally and by using these methods in a way that meshes with the rest of the curriculum. More disciplined and formal thinking should pervade the curriculum: if it is in a separate course, students will think it is a separate thing from system building. This education is necessary if we are to achieve high confidence programming. Today, most students do not know that their programs are not correct -- they do not try them on enough test cases. If, however, they are told that they will get a zero for the assignment unless the program gives reasonable error messages on a number of test cases, they may try harder. Universities and industry have to join in partnership to transfer university developed technology (i.e., the research prototypes) into usable industry technology. We must also transfer the research prototype to commercial systems developers where the cost per individual failure is low, but there are many copies of the product (e.g., hardware failures). We then would be able to amortize the total cost across all these copies; the collective cost may actually be quite high. The key to this solution is forging the appropriate partnerships between the tool developers and the problem holders. As part of technology transfer, researchers have an obligation to learn about the pressures underlying product development. The methods we are developing should not have a huge learning curve, and it should not require a lot of time to build specialized models. We should maximize the use of "semi-formal" and informal methods, and have a focused use of formal methods on the most critical or difficult part of the product. We must consider human factors for users for developers. Such human factors can be applied to notations and tools (e.g., to make it easier for a developer to translate a specification into code). Human factors can also be applied to administrator interfaces. Most administration interfaces allow users to do bad things without any warning. We must seek compromise, not victory. For example, if you use this methodology, you can get a certain kind of help. Understanding the utility of compromise is important; even in critical systems it is often the simple components that people are getting wrong; they need better type checkers, for example. Give them the simple components now and you are better situated to give them more later. We must learn from the mistakes of others. How else are we to know, in advance, where to focus attention for the application of formal methods? We must understand where systems break down. This may require looking across many cases and developing meaningful statistics. Since today's systems are low-confidence systems, there should be enough cases to generate statistics. For example, we might not have known in advance that buffer overflows would turn out to be such a common security problem, but after we see so many examples of this, we should know to focus attention on buffers. It is becoming more likely that many of our critical systems will be deployed with Windows. We will feel its effects (e.g., new software may make the job take longer, or when the computer is down the lines will get longer at the airport). It is not commonly understood how weak these commodity products are. Products used in critical systems must be simple enough so that we can analyze their failure modes. Can you build high confidence systems from low-confidence parts? We can learn from practices developed for trusted systems. A lot of the functionality is probably not safety oriented, so we should concentrate our efforts on the areas that are safety critical and protect those areas. For example, only put Windows where it is not safety critical. The increasing prevalence of virtual machines may make high confidence easier. If the Java Virtual Machine (JVM) really does run on every platform, it could help in two ways: (1) increasing the uniformity of the execution environment would allow people to better focus their efforts on creating a high confidence execution environment; and (2) if it has higher assurance than what people were using before, it is an immediate win. |
|
|
|
|
Research-Supported Education
|
Today's systems are highly complex, especially embedded control systems for ships, aircraft, automobiles, factories, weapons, nuclear power plants, and medical devices. They have a lot of software, legacy components, and commercial hardware and software, all pulled together by a domain-defined fabric. These systems are often distributed, highly interconnected, highly integrated, and operationally time-constrained. They have a significant cost of failure, and such high costs mandate the need to achieve high confidence in their design, construction, maintenance, and operation. Systems fail because of operational wear-and-tear, operator error, and human-induced defects introduced during system design and development. Failure results from incomplete definition of requirements, defects in software or hardware, operational error (e.g., lengthy, complicated, broken procedures), security violations, implementation defects, and human-computer interface designs that lead to operator confusion. They may also fail due to their inherent complexity. There are many interesting recent failures such as the Internet's Domain Name Service (DNS) failure due, in part, to the distribution of bad tables; the America On-Line (AOL) upgrade error; and AT&T's WORLDNET net-wide propagation of a single error in a C program which caused failure of AT&T's long distance service due to a register overflow that, in turn, was compounded by having the backup database overwritten by a corrupted database during recovery. John Knight of the University of Virginia asserted that research-supported education has to be one of the key solution directions. We need education for practitioners that teaches them existing techniques and we also need new techniques for practitioners. The computer science research community has not reached out to engineering. Obtaining new techniques for engineering practitioners requires that we educate researchers in the context of practical issues and practical constraints. Such education requires a multi-disciplinary, coordinated research program. Bad technology continues to be used by practitioners. We must inform practitioners about the good technology that exists but is not widely used, such as "semi-formal" specifications, strongly typed languages, test tools and techniques, static analysis and inspection, and rigorous and analyzable design techniques. Predicate calculus should be taught and understood by any engineer. Promising new technology needs to be tried more widely, such as formal specification, application generators, component-based reuse, test case synthesis, etc. But some of these things are not quite ready for prime time. We can learn how to make them more robust from experimenting with their use. Researchers must be educated so that they understand what they need to work on. They must understand the real problems and issues, the environment, and the priorities. If researchers do not understand these things, they will be working on the wrong problems. People do not jump into new technologies rapidly; researchers need to understand the concepts and tools that the engineers use to accomplish their work. Researchers need to give the engineers specification constructs and tools that the engineers can understand. The concepts and tools that are produced and used should focus a practitioner's energy where it should be focused. For example, engineers prefer to use switching diagrams, LaPlace diagrams, etc., because they are skilled in their use and the notation allows them to focus attention on the problem rather than on the notation. This then leads to the requirement to better integrate tools across the disciplines, and more research is needed to accomplish such integration. Another participant pointed out that we vitally need practitioner education to reduce over-simplified ad hoc solutions in fielded critical systems, such as n version, unsynchronized fault tolerance. Design problems (e.g., meeting both security and reliability needs) are fairly sophisticated, and ad hoc solutions are being used on life-critical systems such as the Boeing-777 channel control systems and train control systems, developed by engineers lacking necessary knowledge about advances in high confidence systems techniques. Almost no articulated knowledge exists in these fields that is written down; most knowledge is passed on verbally within an organization. Such verbal lore is highly localized. We must bring such knowledge to higher levels of visibility. |
|
|
|
|
Engineering Process Integration
|
Shiu-Kai Chin from Syracuse University proposed that solutions will come from reducing theory to practice for high confidence design. Chin is working on an educational program whose goal is to have a lasting impact on our high confidence systems through change and focused improvements to our systems engineering processes. He believes this lasting impact will result from teaching engineering students abstract conceptualization and applying it to small examples in the classroom. Chin noted that the 1995 CIC report has been a strong influence on the directions of his program at Syracuse University. He is developing and teaching masters-level courses in engineering, and his students are using formal techniques for high confidence system design. He wants to move formal methods for high confidence into undergraduate education. He believes that predicate calculus is appropriate for undergraduate engineering students and that they can absorb it if there are sufficient examples for them to work through. Chin is engaging high confidence systems engineering along two dimensions: (1) developing support for reasoning, evaluation, and conformance; and (2) developing a science of composability and its application to engineering. What he hopes to achieve is an enhanced, multi-disciplinary design process that uses several formal methods and tools in an integrated fashion. In developing his integrated approach, Chin asks several key questions:
System engineering requires integration of many design methods, tools, and techniques; connections should be encouraged among them. Chin referred to David Kolb's 1984 experiential learning cycle (characterized as "concrete experience -> reflective observation thinks -> abstract conceptualization -> active experimentation") and noted that our research processes are out of synch with our software development processes. Industrial engineering has generally been on only two parts of the cycle (active experimentation and concrete experience), while academic researchers have been in the other two parts of the cycle. We must connect the two loops -- feeding problems to the research community and solutions back to the development community. Chin wants to show that formal methods and tools are of practical value in an enhanced design process. His approach is to provide one or more concrete challenge problems (similar to the DARPA/NSA/DISA Joint Technology multi-level security (MLS) formal methods challenge problem) to demonstrate the utility of formal methods. A challenge problem must be a real system with properties to be established. Chin intends to incorporate into his enhanced design process the support necessary for assurance and synthesis through formal verification and compilation. He is interested in showing the potential for starting from a top-level requirement and achieving a synthesized set of code. He is including higher order logic and functions to support parameterized design and use of hardware and software components. Compilation from higher order logic theories and algebraic specifications is used to produce C++ code. He separates the data path and control path operations for analysis. This separation sets up the verification path and the synthesis path. It is easy to show the relationship of these paths (e.g., using Kestrel's Specware category theory-based tool). There are appropriate points of correspondence that can be used to join them. Chin has used Specware to generate code for a secure e-mail system. Unifying various logics could mean a potential wait of twenty years. But there are more practical approaches. In a year, Chin established a correspondence mapping between synthesis (refinement in Specware) and verification (type definition in HOL (high order language)). Chin mentioned the 21st Century Engineering Consortium, which will focus on education and how to move formal methods for high assurance design into mainstream engineering. An initial two-day workshop is being held in Melbourne, Florida, in March 1998. The workshop is intended to gather insights from industry and government, identify what skills are needed, and to examine current practices in education. Two questions are to be answered: What are we teaching and why? How well are we doing? The answers are intended to be the source of recommendations for both graduate and undergraduate education. |
|
|
|
|
Improved Use of Programming Languages
|
Peter Lee from Carnegie Mellon University brought two related examples of potential solutions to the table from his research focus on improving our use of programming languages to achieve higher confidence systems. Lee asserted that the science of programming languages is a bridge between research and practice. We should have no distinction between programming and specification languages. Such languages provide the structure for communicating, either to another human or to a computer or both. Programming languages also give you a way of mediating the boundary between formal and informal methods. Programming languages provide an essential foundation for high confidence computing. Lee illustrated the contribution of programming languages to high confidence using the analogy of maze puzzles. A good maze must have a solution; and both the maze producer and the user want confidence in that condition. Now, suppose a maze extends infinitely in two dimensions. It is extremely difficult to know if such a maze has a solution. But if a maze producer wants to convince a maze "consumer" that the maze is a good maze, he can provide the solution path along with the maze, and the consumer can simply check it. It is much easier to check a solution than to generate it. The consumer does not care how the line trace was generated or derived. Lee presented a similar approach for high confidence software. At Carnegie Mellon, Lee is directing the Fox project, that is conducting research in the composition of software. The programming language solution to composition is to use interfaces, that is, one can check whether two interfaces can match up. But the problem is we can not know if an imported software component (say an applet) will do bad things to another component. So the solution is to require that imported code come with some "witness" to the fact that it follows our rules. This witness approach Lee calls Proof-Carrying Code (PCC). PCC is a technique that packages the proof of a software module's properties along with the module's executable code. This makes it possible to check the module against an application's specification before including the module. PCC has several advantages:
Checking imported modules against application-specified pre-conditions provides higher confidence of correct operation. Lee, along with George Necula, has been applying this to the context of extensible operating systems. They are implementing PCC in a Unix kernel. Their formal safety policy is a local (kernel) definition of what should happen or should not happen. But they still have the problem of how to know if they have formally stated what they wanted to state or what they should have stated. They are working on several program proofs in the areas of high-speed networking and extensible operating systems. These include bounds checking; memory safety; time limits (actually instruction count limits); and resource constraints such as guaranteed memory deallocation, locks, and network I/O (guarantee write constraints of no more than n packets per second). They are also working on a proof that target code produced by an optimizing compiler preserves the type safety properties of the source code (for Java) and a proof that a machine language program meets the type safety properties of machine language (ML). Example proofs were checked five to fifteen times faster than software (pretty good privacy -- PGP) encryption. Lee stressed the role of types and type theory in providing high confidence. An example from his research shows that in using modern programming languages (e.g., ML) a safety predicate can be encoded as a type. With the proof encoded as an expression of that type, proofchecking is reduced to typechecking. Type checking then becomes a means to guarantee the (type) safety property. In his work, the proofs are represented in a type system (line feed (LF)) because LF typechecking is decidable. Standard techniques from type theory are used to prove the soundness of all of this and to obtain better algorithms for fast checking of proofs and more compact encodings. And because it is a programming language, there is a bridge from the formal analysis to the actual implementation. To date, these proofs have been generated by hand, but it is hard work. Lee and Necula want to do proof generation. Several research questions arise: Can we have a compiler generate these proofs, and can we avoid having to do theorem proving on the compiler? Can we preserve properties all the way down to machine code? Can we prove that the compiler has not fouled something up? Experience has shown that simple properties (memory safety, instruction counts, etc.) for simple programs (e.g., packet filters) seem to be no problem, but scaling to more interesting properties remains an issue. Peter Lee thinks that we can do type-directed compilation. His approach of propagating types and staged type checking may provide an answer. Carrying type information across intermediate levels of translation and checking it at each pass of compilation is a possible approach to certifying compilers. This could serve as assurance for the correctness of the compiler without formal theorem proving; it can propagate easily checked safety information all the way to native code. Lee thinks that programming language theory should be part of any high confidence program. While providing potential solutions, much remains for further research. These include advanced programming languages, type theory, formal semantics, and applications of logic. Basic research on foundations is needed. Higher assurance in operating system kernels has been achieved through the application of type theory (LF type theory in the Open Group's OSF/1 kernel). Research on the application of programming language theory is spreading. It is being applied to networks and operating systems as well as to security, real-time computing, and distributed computing. Programming language theory may be entering a golden age: theorists are becoming aware of problems in related areas of computer science and it is sparking a lot of research. However, we have also seen a heavy shift away from basic research. The U.S. is still behind Europe in this theoretical area. We have a serious shortage of fresh talent. And there is the growing perception by researchers (possibly real) of no interest from Government organizations and funding agencies. |
|
|
|
|
Endnotes |
|
|
|
|
|
|
|
