postdoc position in Toulouse on lightweight formal architecture specification

postdoc position in Toulouse on lightweight formal architecture specification

[David CHEMOUIL]

Dear colleagues,


A post-doctoral position is available in Toulouse, France, jointly
proposed by Onera/DTIM and IRIT.

Keywords: Formal specification, formal verification, lightweight formal 
methods,
software architecture.

PDF version here: 
<http://www.onera.fr/sites/default/files/u491/20140121-postdoc-formal-spec-archi.pdf>

Location : Toulouse, France
Onera supervisors : Julien Brunel & David Chemouil
--> Mail: firstname.lastname@onera.fr
IRIT supervisor: Jean-Paul Bodeveix
--> Mail: lastname@irit.fr

Subject
=======

This subject fits into a joint research effort by Onera/DTIM and IRIT to
devise lightweight formal methods for the specification and verification
of dynamic software architecture.

Architecture  describes a system in terms of abstract concepts (e.g.,
components, connectors, configurations, behaviour contracts) and
addresses extra-functional properties, while still enabling to draw a
correspondence with higher-level requirements. Architecture Description
Languages (ADLs) provide views focused on expressing the structure and
the behaviour of a system as a composition of components and connectors.
The formal specification and verification of behavioural properties of
components and/or connectors have mainly been addressed using
process-algebraic techniques (e.g., CSP for Wright , the \pi-calculus
for Darwin ) or automata (e.g., constraint automata for coordination in
Reo , various contract theories ). Finally, CommUnity  is a notable
approach relying on categorical methods to give an abstract account of
various architectural concepts. Nevertheless, although studied in some
works, some interesting questions, such as that of a more abstract
specification language or that of formal refinement, have not been
developed as thoroughly as in formal specification and lack tool
support.

Formal specification methods, indeed, such as Z , B  (and more recently
Event-B ) or VDM , often adopt a more abstract view than the ones cited
above. These methods rely on expressive logics and promote formal
refinement techniques. However, they are not very well suited to
addressing architecture concerns as architectural elements (e.g.,
component and connector instances) are not first-class concepts.
Furthermore, formal verification can only be partially automated because
of the very expressiveness of the underlying logics.

This last remark led to the development of Alloy  which trades some
expressiveness in favor of automated bounded verification based on SAT
techniques. This approach, dubbed lightweight by its author as it
promotes “agility” (quickly-available feedback of automated verification
of small models) over the exhaustivity of more traditional formal
methods, is surprisingly efficient in practice. Indeed, even if the
verification is not complete, many intricate errors can be spotted for a
relatively low modelling and verification effort. Nevertheless, as of
now, Alloy does not feature first-class concepts to model behaviour nor
architectural concerns (although some propositions exist, in particular
for the former aspect).

In this context, Onera/DTIM and IRIT are investigating the development
of a lightweight formal specification approach for (possibly real-time)
software architecture. The aim is thus to allow the “declarative”
specification of behavioural and architectural concerns and the
automated verification thereof. The present postdoctoral position takes
place in this setting. Applicants should (be about to) hold a PhD in
formal methods or theoretical computer science and should be willing to
participate actively in the objective sketched above. The exact
contribution will depend on the retained candidate and we are open to
suggestions. For example (this is only indicative!), one may think of:

-   devising a new temporal logic providing a formal basis for the
     method

-   providing a formal semantics to the specification language

-   devising a categorical framework to account for composition or
     behaviour

-   developing SMT-based (SAT modulo theories) verification techniques
     (e.g., to address real-time aspects)…

Application
===========


-   Applicants should send a resume via email to David Chemouil and
     Jean-Paul Bodeveix.

-   Applicants are expected to be fluent in English or in French
     (possibility of French courses).

-   Position duration: 1 year.

-   Gross salary: ~2,500 €/month (position funded by RTRA STAE, a
     French science foundation for space and aeronautics research).



_______________________________________________
Concurrency mailing list
Concurrency@listserver.tue.nl
http://listserver.tue.nl/mailman/listinfo/concurrency

postdoc position in Toulouse on lightweight formal architecture specification

[David CHEMOUIL]

Dear colleagues,


A post-doctoral position is available in Toulouse, France, jointly
proposed by Onera/DTIM and IRIT.

Keywords: Formal specification, formal verification, lightweight formal
methods,
software architecture.

PDF version here:
<http://www.onera.fr/sites/default/files/u491/20140121-postdoc-formal-spec-archi.pdf>

Location : Toulouse, France
Onera supervisors : Julien Brunel & David Chemouil
--> Mail: firstname.lastname@onera.fr
IRIT supervisor: Jean-Paul Bodeveix
--> Mail: lastname@irit.fr

Subject
=======

This subject fits into a joint research effort by Onera/DTIM and IRIT to
devise lightweight formal methods for the specification and verification
of dynamic software architecture.

Architecture  describes a system in terms of abstract concepts (e.g.,
components, connectors, configurations, behaviour contracts) and
addresses extra-functional properties, while still enabling to draw a
correspondence with higher-level requirements. Architecture Description
Languages (ADLs) provide views focused on expressing the structure and
the behaviour of a system as a composition of components and connectors.
The formal specification and verification of behavioural properties of
components and/or connectors have mainly been addressed using
process-algebraic techniques (e.g., CSP for Wright , the \pi-calculus
for Darwin ) or automata (e.g., constraint automata for coordination in
Reo , various contract theories ). Finally, CommUnity  is a notable
approach relying on categorical methods to give an abstract account of
various architectural concepts. Nevertheless, although studied in some
works, some interesting questions, such as that of a more abstract
specification language or that of formal refinement, have not been
developed as thoroughly as in formal specification and lack tool
support.

Formal specification methods, indeed, such as Z , B  (and more recently
Event-B ) or VDM , often adopt a more abstract view than the ones cited
above. These methods rely on expressive logics and promote formal
refinement techniques. However, they are not very well suited to
addressing architecture concerns as architectural elements (e.g.,
component and connector instances) are not first-class concepts.
Furthermore, formal verification can only be partially automated because
of the very expressiveness of the underlying logics.

This last remark led to the development of Alloy  which trades some
expressiveness in favor of automated bounded verification based on SAT
techniques. This approach, dubbed lightweight by its author as it
promotes ???agility??? (quickly-available feedback of automated verification
of small models) over the exhaustivity of more traditional formal
methods, is surprisingly efficient in practice. Indeed, even if the
verification is not complete, many intricate errors can be spotted for a
relatively low modelling and verification effort. Nevertheless, as of
now, Alloy does not feature first-class concepts to model behaviour nor
architectural concerns (although some propositions exist, in particular
for the former aspect).

In this context, Onera/DTIM and IRIT are investigating the development
of a lightweight formal specification approach for (possibly real-time)
software architecture. The aim is thus to allow the ???declarative???
specification of behavioural and architectural concerns and the
automated verification thereof. The present postdoctoral position takes
place in this setting. Applicants should (be about to) hold a PhD in
formal methods or theoretical computer science and should be willing to
participate actively in the objective sketched above. The exact
contribution will depend on the retained candidate and we are open to
suggestions. For example (this is only indicative!), one may think of:

-   devising a new temporal logic providing a formal basis for the
      method

-   providing a formal semantics to the specification language

-   devising a categorical framework to account for composition or
      behaviour

-   developing SMT-based (SAT modulo theories) verification techniques
      (e.g., to address real-time aspects)???

Application
===========


-   Applicants should send a resume via email to David Chemouil and
      Jean-Paul Bodeveix.

-   Applicants are expected to be fluent in English or in French
      (possibility of French courses).

-   Position duration: 1 year.

-   Gross salary: ~2,500 ???/month (position funded by RTRA STAE, a
      French science foundation for space and aeronautics research).





[For admin and other information see: http://www.mta.ca/~cat-dist/ ]