Hi Horace,
the version number in the abstract spec document is wrong, it should read 3.2.x. It looks like we missed this one when we changed our release process and it’s been sitting at 1.3 forever. Thanks for alerting us.
You can generally see which version combination of l4v and seL4 fit together by examining https://github.com/seL4/verification-manifest
It has official release versions such as 3.2.0.xml and it shows the combination of current development revisions in default.xml.
To explore the spec in Isabelle/jEdit I’d load the file spec/abstract/Syscall_A.thy and let Isabelle process it - the toplevel entry point is the function call_kernel at the bottom of that file. You can go from there, using Command/Ctrl click on constants to jump to their definitions etc.
To get there, you first have to pick an architecture, e.g. in l4v/
export L4V_ARCH=ARM isabelle/bin/isabelle jedit -d . -l Word_Lib spec/abstract/Syscall_A.thy
Cheers, Gerwin
On 09.08.2016, at 01:11, Horace Blanc horaceblanc@gmail.com wrote:
Hi,
I would like to know if the verification of the seL4 is up-to-date with the newest version of the sel4 microkernel (3.2.0). If so, how do I access it? When I run make ASpec in l4v, I get a pdf with the Abstract Formal Specification in version 1.3. Does it refer to the seL4 microkernel version 1.3 or has the Abstract Formal Specification its own versions?
Also, what is the best way to explore this specification in Isabelle/jedit?
thanks in advance
Horace Blanc
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel