The Languages and Tools group devises sophisticated techniques and models for understanding software systems, programs and programming abstractions based on powerful mathematical abstractions. The group develops related design and implementation technology to demonstrate the viability of those techniques to support developers in managing the ever increasing complexity of modern software.
Design Space Exploration – Design space exploration (DSE) is the process of enumerating and ranking completions of partial system design descriptions while satisfying a (possibly huge) number of design constraints with complex interdependencies. Because of those interdependencies, system architects must consider all design constraints very early in the system design process to ensure a proposed system architecture will eventually lead to an implementation satisfying all requirements. DSE helps architects in evaluating design alternatives and choosing an appropriate architecture. Mathematically, DSE can be considered a constraint satisfaction problem. The tool FORMULA uses constraint logic programming (CLP) and satisfiability modulo theories (SMT) to solve those kinds of problems.
Software Verification – EMIC’s software verification efforts are focused on the development and application of a “Verifier for Concurrent C (VCC)”. VCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them. In contrast to testing, verifying a piece of code establishes its correctness for all possible inputs and execution paths (100% coverage), which is particularly helpful for complex concurrent code where it is very hard to establish acceptable coverage with testing. VCC extends C with design by contract features, like pre- and post-conditions as well as type invariants. Today, VCC is the only verifier for C that works function- and thread-modular, which means that it scales to large code bases independently of the number of functions or threads. VCC annotations are transparent to a C compiler. They do not change the compiled code and therefore do not impact runtime behavior.
Embedded Systems – Modern embedded systems, such as the control system in a vehicle or the control of production processes in a factory, are distributed communicating systems whose sensors, actuators and computing nodes provide increasingly complex functionality. Moreover, these systems have to meet tight non-functional requirements in terms of their real-time behavior, memory footprint, or energy consumption. DSE helps to design those systems with better quality, fewer design iterations, and increased cost-effectiveness.
IT Management – Managing IT infrastructures requires keeping the software and configurations of hundreds or thousands of computing devices in sync – ranging from servers to PCs to smart phones or a host of embedded devices. IT administrators must match user requirements with corporate requirements and technological constraints to determine which version of what software must be installed and how it must be configured on a particular device. DSE helps administrators to makes sense of those different constraints, make smart decisions from among the myriad of different configuration options and keep their infrastructure in a healthy state.
Operating Systems and Data Base Systems – Operating systems stopped being single threaded 20 years ago. Today, they are extremely complex pieces of concurrent software that extensively use the features of the underlying hardware to execute quickly and securely. Because of this complexity, it is increasingly difficult and costly to assure the desired quality of operating system code by testing. Formal verification is an alternative that today, after more than 30 years of research, approaches practical viability. VCC has been used to verify the core of Microsoft’s hardware virtualization solution Hyper-V, which consists of 100,000 lines of concurrent C code. Similarly, data base systems face extreme performance requirements. To address those requirements, they use very aggressive optimizations, such as lock-free algorithms in transaction kernels. These algorithms are very complex and difficult to debug. Again, formal verification with VCC can establish the correctness of the implementation and prove that not only the algorithm but also its implementation is safe.
- Moritz Y. Becker, Alexander Malkis, and Laurent Bussard, A Practical Generic Privacy Language, in Sixth International Conference on Information Systems Security (ICISS 2010), Springer Verlag, December 2010.
- Moritz Y. Becker, Alexander Malkis, and Laurent Bussard, S4P: A Generic Language for Specifying Privacy Preferences and Policies, no. MSR-TR-2010-32, April 2010.
- Muhammad Ali, Laurent Bussard, and Ulrich Pinsdorf, Obligation Language and Framework to Enable Privacy-aware SOA, in Data Privacy Management and Autonomous Spontaneous Security, Springer, March 2010.
- Ethan K. Jackson, Eunsuk Kang, Markus Dahlweid, Dirk Seifert, and Thomas Santen, Components, platforms and possibilities: towards generic automation for MDA, in EMSOFT, ACM, 2010.
- Laurent Bussard, Anna Nano, and Ulrich Pinsdorf, Delegation of access rights in multi-domain service compositions, in Identity in the Information Society, vol. OnlineFirst, Springer Verlag, December 2009.
- Laurent Bussard and Moritz Y. Becker, Can Access Control be Extended to Deal with Data Handling in Privacy Scenarios?, in W3C Workshop on Access Control Application Scenarios, November 2009.
- Moritz Y. Becker, Alexander Malkis, and Laurent Bussard, A Framework for Privacy Preferences and Data-Handling Policies, no. MSR-TR-2009-128, September 2009.
- Stefan Brands, Laurent Bussard, Joris Claessens, Christian Geuer-Pollmann, and Ulrich Pinsdorf, Identity Management in Service Oriented Architectures, in The Future of Identity in the Information Society, pp. 167–171, Springer, June 2009.
- Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies, VCC: A Practical System for Verifying Concurrent C, in Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Springer, 2009.
- Ethan K. Jackson, Dirk Seifert, Thomas Santen, Nikolaj Bjørner, Wolfram Schulte, and Markus Dahlweid, Specifying and Composing Non-functional Requirements in Model-Based Development, in Proceedings of the 8th International Conference on Software Composition, Springer Verlag, 2009.