From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7986 Path: news.gmane.org!not-for-mail From: David CHEMOUIL Newsgroups: gmane.science.mathematics.categories Subject: postdoc position in Toulouse on lightweight formal architecture specification Date: Tue, 21 Jan 2014 17:29:40 +0100 Message-ID: Reply-To: David CHEMOUIL NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit X-Trace: ger.gmane.org 1390356144 22139 80.91.229.3 (22 Jan 2014 02:02:24 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 22 Jan 2014 02:02:24 +0000 (UTC) To: asr-forum@cines.fr, categories@mta.ca, Original-X-From: majordomo@mlist.mta.ca Wed Jan 22 03:02:33 2014 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.186]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1W5n9C-0006HY-23 for gsmc-categories@m.gmane.org; Wed, 22 Jan 2014 03:02:30 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:44857) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1W5n7Y-0003p0-PF; Tue, 21 Jan 2014 22:00:48 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1W5n7Z-0007hs-8x for categories-list@mlist.mta.ca; Tue, 21 Jan 2014 22:00:49 -0400 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7986 Archived-At: 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: 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/ ]