The following content has been provided by the University of Erlangen-Nürnberg.

Thanks for the introduction and for having me here. So the title of my talk is Proof-Caring

Services, and this is also the name of a sub-project in the Colorado Research Center on the Flight

Computing that we are running currently in Paderborn. So I would like to talk about three

things. First, to give a very brief and that would be also a very shallow overview over

the CRC, what the mission is and what kind of research is being done there. Then I will

focus more on what's the title of my talk, Proof-Caring Services. I will basically explain

what we understand on the Proof-Caring Services, and this is a special issue, Proof-Caring

Hardware, which is more or less my area of research in this sub-project. And then I will

in the third part zoom in even more and talk about one specific topic in this Proof-Caring

Hardware area, which is actually a combination of Proof-Caring Hardware and Proof-Caring

Code, so verification of software and hardware altogether. And finally we'll sum up. So starting

with the vision of our CRC. So the vision is that in future, software will not be like

today, mostly in huge monolithic packages. It will be on the fly, configured and executed

out of very small services. So that means that the software should be a highly personalized

and individualized service. And the small services that are available, they would be

traded on world-wide markets. This is kind of the vision that some software people have

and that drove this kind of setup of the CRC. And also such markets do not exist today.

So another issue is also that such markets need to be organized. So the players on the

market need to be identified, the incentives, the business models, and so on. So putting

this together, there's of course a number of known research areas that would contribute

to such a vision. For example, the configuration of software services. There is today something

like software-oriented architectures, which could be seen as a starting point for these

kind of service markets. The execution, that could be cloud computing, but we envision

not a computing infrastructure as cloud computing today, which is mostly homogeneous machines.

We envision much more higher dynamics and heterogeneity. Distributed computing has a

lot of things to offer for the technical markets infrastructure, which is networks and distributed

computing. And mechanism design is a main underlying area for organization of markets.

I would like to start to show with an example, an example how we envision how this could

work. So there is a customer. The customer could be, in this example, say the community

of Paraborn that wants to optimize or lay out maybe the water supply networks, the pipes

and all kinds of towers and so on. And that would be the customer. So this customer then

goes to a specific person, which is in our terminology a service provider for optimization.

So water pipes need to be optimized. And that is a person or an entity that can provide

these optimization services domain specifically. So domain is optimization. And this person

knows that, after talking to the customer, that in order to do these kind of optimization

jobs, following things are needed. There is a data management system needed, model generation,

then solvers, depending on what kind of models these are, continuous, discrete, et cetera,

et cetera. Visualization is a typical part here. Decisions are brought. And eventually

the complete application that is then configured has to be executed somewhere. So in order

to come up with an offer for the customer, the service provider would then on the worldwide

markets contact providers for single software components and also for compute services.

There might be many offers for solvers that are around. And the ODS service provider would

make sure that the things that are being selected work together properly and fulfill the request

of the customer. So this was actually our application example that we had in the first

phase of the CRC, because we had expertise in that in part of one. But of course, this

is not really on the fly market that we're wishing for future, because in this optimization

business there are still software packages which are quite big, optimizations, solvers,

big visualization tools, and so on. And also this looks like a one-dimensional chain. So

in general, it could be a graph.