Hi Oscar,

I think for ELISA members, it would especially interesting to understand what the current state and progress is on your tool qualification of gcc, especially in the context of a Linux kernel compilation. I also think that the gcov qualification is interesting in this context as well.

As you probably know, a Linux kernel compilation requires quite some functionality from the gcc compiler. Getting Linux compiled with clang did take years of effort as Linux puts quite some requirements on a compiler, but we are now close to have a second compiler. That might allow another tool qualification strategy.

I do not see that everyone will be able to meet in person in the next few weeks. Should we schedule an online meeting to explain your goal, your approach and the current state?

@all: Who else would be interested in such a webex for the presentation of this topic?

Best regards,

Lukas

Von: devel@... [mailto:devel@...] Im Auftrag von slotosch@...
Gesendet: Montag, 25. März 2019 15:16
An: devel@...
Betreff: Re: [devel] Brainstorming on potential activities

Hi Lukas, hi all,

It’s many years ago that we presented our ideas about tool qualification in the OSDAL group.

Meanwhile we have evolved to a word wide leading provider of tool qualification kits and provide

Qualification kits for tools, libraries and SEOOCS compliant to ISO 26262 and IEC 61508 with our certified qualification process.

We are happy to update you on our recent thoughts and methods how to build a QKit for Linux.

We see three different classes of elements in ISO 26262 and IEC 61508 as part of the “safety architecture”:

-         - Tools

-         - Unchanged/pre-existing software components

-         - Software (SEOOCs)

And we think that Linux requires qualification for elements within all those classes.

So therefore we propose as potential activities for Elisa:

·         * Description of a process for qualification of Linux and Linux applications

·         * safety plan, showing the compliance of the process with ISO 26262 and IEC 61508 (including of checks to be performed)

·         * qualification of

o   linux tools for

- compilation, e.g. gcc

-  code coverage measurement, e.g. gcov

-  test automatization, e.g. gtest, gdb

o   Linux libraries , libc, libm, C++stdlibs (as far as needed)

o   Linux components, e.g. kernel, modules

·         * Provide a qualified tool chain to safely develop applications

The following things we have already achieved and can present you within one of our next meetings (in case you are interested)

·         (certified) qualification processes for Tools & Libraries (SEOOCs still open)

·          - QKit for gcc

·          - QKit concept for gcov

·          - QKit for 200 runtime functions of libm, libc

·          - QKit for QKits (adaptable for linux)

So we think there is much to do, but we do already have parts, plans & visions that we like to share with you in case this is interesting for you.

Kind regards,

                Oscar Slotosch

--

Validas AG

Dr. Oscar Slotosch

Vorstand

mailto:slotosch@...

http://www.validas.de

fon: +49 (0) 89 / 53 88 669-11

fax: +49 (0) 89 / 53 88 669-10

--

Validas AG

Firmensitz: Arnulfstr. 27, D-80335 München

Registergericht: Amtsgericht München HRB 131653

Vorstand: Dr. Oscar Slotosch, Dr. Peter Braun

Aufsichtsratsvorsitzender: Prof. Dr. Dr. h.c. Manfred Broy

Hi Evgeny,

I think this is also a good topic for a presentation to the people interested in ELISA.

@all: Who would be interested in the presentation of the current state of Klever and ideas for future development?

Best regards,

Lukas

Von: devel@... [mailto:devel@...] Im Auftrag von Evgeny Novikov
Gesendet: Montag, 8. April 2019 10:09
An: devel@...
Betreff: Re: [devel] Brainstorming on potential activities

Hi all,

In thread “Collection of pre-existing activities, work, concepts and ideas” I presented you software verification framework Klever. Concerning verification of the Linux kernel, this framework already demonstrated an ability to detect faults, many of which can be hardly found out by other techniques. Besides, it has a huge potential. We consider possible directions for further development of Klever that can contribute verification of the Linux kernel in some way in this document.

If anybody is interested in enabling formal methods for the Linux kernel, we would be glad to discuss this. Everything related with verification of the Linux kernel in Klever is open source. And you can easily join the development team.

--
Evgeny Novikov
Linux Verification Center, ISP RAS
http://linuxtesting.org

Hello,

Is there already a meeting schedule, where the presentations & discussions shall be hold?

Kind regards,

                Oscar

PS

We also like formal methods and have recently be building a QKit for a formal method tool (in a research project),

Allowing to cover more aspects from the safety standards (verification, flow analysis, programming guidelines?..)

as by saying “.. can contribute to the verification”.

So we would be interesting to discuss this Klever and the credits for the process.

Hi Evgeny,

I think this is also a good topic for a presentation to the people interested in ELISA.

@all: Who would be interested in the presentation of the current state of Klever and ideas for future development?

Best regards,

Lukas

Von: devel@... [mailto:devel@...] Im Auftrag von Evgeny Novikov
Gesendet: Montag, 8. April 2019 10:09
An: devel@...
Betreff: Re: [devel] Brainstorming on potential activities

Hi all,

In thread “Collection of pre-existing activities, work, concepts and ideas” I presented you software verification framework Klever. Concerning verification of the Linux kernel, this framework already demonstrated an ability to detect faults, many of which can be hardly found out by other techniques. Besides, it has a huge potential. We consider possible directions for further development of Klever that can contribute verification of the Linux kernel in some way in this document.

If anybody is interested in enabling formal methods for the Linux kernel, we would be glad to discuss this. Everything related with verification of the Linux kernel in Klever is open source. And you can easily join the development team.

--
Evgeny Novikov
Linux Verification Center, ISP RAS
http://linuxtesting.org

Hi Oscar,

the meeting schedule is up to the members of this mailing list to define.

I would hope that those that are interested, answer here by email, then we determine the best time slot to reach everyone during their day time in their time zone and propose different dates in a doodle to find the best date.

If we pick up more and more topics, we can actually plan a fixed time slot every week (or every two weeks), but let us first see how many presentations and topics of discussion are proposed.

Best regards,

Lukas

Hello,

Is there already a meeting schedule, where the presentations & discussions shall be hold?

Kind regards,

                Oscar

PS

We also like formal methods and have recently be building a QKit for a formal method tool (in a research project),

Allowing to cover more aspects from the safety standards (verification, flow analysis, programming guidelines?..)

as by saying “.. can contribute to the verification”.

So we would be interesting to discuss this Klever and the credits for the process.

Hi Evgeny,

I think this is also a good topic for a presentation to the people interested in ELISA.

@all: Who would be interested in the presentation of the current state of Klever and ideas for future development?

Best regards,

Lukas

Von: devel@... [mailto:devel@...] Im Auftrag von Evgeny Novikov
Gesendet: Montag, 8. April 2019 10:09
An: devel@...
Betreff: Re: [devel] Brainstorming on potential activities

Hi all,

In thread “Collection of pre-existing activities, work, concepts and ideas” I presented you software verification framework Klever. Concerning verification of the Linux kernel, this framework already demonstrated an ability to detect faults, many of which can be hardly found out by other techniques. Besides, it has a huge potential. We consider possible directions for further development of Klever that can contribute verification of the Linux kernel in some way in this document.

If anybody is interested in enabling formal methods for the Linux kernel, we would be glad to discuss this. Everything related with verification of the Linux kernel in Klever is open source. And you can easily join the development team.

--
Evgeny Novikov
Linux Verification Center, ISP RAS
http://linuxtesting.org

All:

I am interested in the both topics, but the gcc topic is much more interesting/important to me. As for meeting times, I greatly prefer afternoon European time (I’m in California, but I’m up early, so any time after 2pm CET can work).

Thanks;

Rob

Robert Bates - Chief Safety Officer Automotive, Mentor a Siemens Business

robert_bates@... | Office: 510.354.5734 | Cell: 408.203.7523

I’m also interested, thanks

Antonio

Hi all,

In thread “Collection of pre-existing activities, work, concepts and ideas” I presented you software verification framework Klever. Concerning verification of the Linux kernel, this framework already demonstrated an ability to detect faults, many of which can be hardly found out by other techniques. Besides, it has a huge potential. We consider possible directions for further development of Klever that can contribute verification of the Linux kernel in some way in this document.

If anybody is interested in enabling formal methods for the Linux kernel, we would be glad to discuss this. Everything related with verification of the Linux kernel in Klever is open source. And you can easily join the development team.

--
Evgeny Novikov
Linux Verification Center, ISP RAS
http://linuxtesting.org