CS为主Logic/math/philosophy相关的positions

The Theoretical Computer Science Group (Prof. Barbara Koenig) at the
University of Duisburg-Essen, Campus Duisburg (Germany) has one open
PhD position in the project Behaviour-GT paid according to TV-L 13
(full-time). Candidates at post-doc level can also be considered.

For more information have a look at our web pages:

http://www.ti.inf.uni-due.de/
http://www.ti.inf.uni-due.de/research/behaviour-gt/

Project Behaviour-GT - Behaviour Simulation and Equivalence of
Systems Modelled by Graph Transformation
---------------------------------------------------------------

The current trend to model driven software and system development
requires the construction of different kinds of models and model
transformations. In order to validate such transformations, behaviour
preservation and refinement are important, but often neglected issues.

In this project we concentrate on graph transformation as a modelling
language, due to its success in modelling dynamically evolving
graphical structures and system architectures. Up to now, however,
there is no systematic study of behaviour simulation and equivalence
for graph transformation systems. The main aim of this project is to
fill this gap and to apply the corresponding results and techniques to
the problem of behaviour preservation of model transformations.  For
this purpose we transfer on the one hand concepts of behaviour
simulation from operational semantics defined by rewriting systems and
on the other hand concepts of behavioural equivalences from the area
of process algebras to the algebraic theory of graph transformations.

In addition to model transformation in general the results will be
applied to the  special case of model refactoring and to protocol
verification. Moreover, tool support will be provided for behaviour
simulation and equivalence and the results will be evaluated in
several case studies.

We prefer applicants with experience in some of the following topics:
concurrency theory, graph transformation systems, process calculi,
Petri nets and/or model transformation.

Requirements
------------

You should have or should be in the process of obtaining a MSc or
equivalent degree. Prior knowledge about the topics of the projects is
considered an advantage. Good English speaking and writing skills are
demanded, as well as the willingness to learn German.


Your Application
----------------

You can obtain further information by adressing your enquiries to:

Barbara Koenig
barbara_koenig@uni-due.de
tel.: ++49-203-3793397

If you are interested in the position, please send your e-mail
application to the address given above. Your application should
include:

* A description of your interest in the project, including your
motivation and specific qualifications.

* A curriculum vitae, including an abstract of your graduate thesis
and the name of your supervisor.

* If you are interested in a post-doc position, please include
a list of your publications and the names of possible referees.

The application deadline is 9 May 2008.

Doctoral Student Positions Available

            Design and Verification of Embedded Software

                   Embedded System Research Unit
                     Fondazione Bruno Kessler
(formerly part of IRST - Centro per la Ricerca Scientifica e Tecnologica)
                          Trento, Italy

       Deadlines:  May 31, 2008

The Embedded System Research Unit (http://es.fbk.eu) of the Bruno
Kessler Foundation, Trento, Italy, is seeking several candidates for Ph.D
positions.

The Ph.D. studies will be held at the International Doctorate School
in Information and Communication Technologies
(http://www.ict.unitn.it/) of the University of Trento, Italy.

The research activity will be carried out within the Embedded Systems
Unit of the Center for Scientific and Technological Research of the
Fondazione Bruno Kessler.

The research activity will aim at techniques, methodologies and support
tools for the design and verification of embedded systems. In
particular, possible topics will include:

- Embedded Software Design and Verification
- Formal Requirements Analysis
- Design and Verification of Hybrid and Timed systems

The selected candidates will be initially enrolled in a stage and, if
they pass the selection of the Ph.D. school, they will be enrolled as
Ph.D. students. Ph.D. courses will start in Autumn 2008, and the
thesis must be completed in three or four years. People enrolled in a
stage and subsequent Ph.D. courses are expected to move to Trento, and
will receive monetary support during both phases of their activity.

Candidate Profile
=================

The ideal candidate should have an MS or equivalent degree in computer
science, mathematics or electronic engineering, and combine solid
theoretical background and software development skills.

The candidate should be able to work in a collaborative environment,
with a strong commitment to reaching research excellence and achieving
assigned objectives.

Background knowledge and/or previous experience in the following
areas, though not mandatory, will be considered favorably:
- Symbolic Model Checking,
- Propositional Satisfiability,
- Satisfiability Modulo Theory,
- Constraint Solving and Optimization,
- Formal Requirements Analysis,
- Software Verification,
- Software Synthesis,
- Embedded System Design Languages (e.g. Verilog, VHDL, System C, and
System Verilog),
- Safety Analysis (FTA, FMEA).

Applications and Inquiries
==========================

Interested candidates should inquire for further information and/or
apply by sending email to <jobs[at]fbk[dot]eu>.

Applications should contain a statement of interest, with a Curriculum
Vitae, and three reference persons. PDF format is strongly encouraged.

Emails will be automatically processed and should have

      'RIF: ES/phd'

as subject.

The Embedded System Research Unit
=================================

The Embedded Systems Unit consists of about 15 persons, including
researchers, post-Doc, Ph.D. students, and programmers. The
Unit carries out research, tool development and technology transfer in
the fields of design and verification of embedded systems.

Current research directions include:

* Satisfiability Modulo Theory, and its application to the
verification of hardware, embedded critical software, and hybrid
systems (Verilog, SystemC, C/C++, StateFlow/Simulink)

* Formal Requirements Analysis based on techniques for temporal logics
(consistency checking, vacuity detection, input determinism,
cause-effect analysis, realizability and synthesis)

* Formal Safety Analysis, based on the integration of traditional
techniques (e.g. Fault-tree analysis, FMEA) with symbolic
verification techniques.

The unit develops and maintains several tools:

* the NuSMV symbolic model checker (http://nusmv.fbk.eu)

* the MathSAT SMT solver (http://mathsat.fbk.eu)

* the Formal Safety Analysis Platform FSAP (http://fsap.fbk.eu)

* the Requirements Analysis Tool RAT (http://rat.fbk.eu)

The unit is currently involved in several research projects, funded by
the European Union (FP VI and FP VII), the European Space Agency, the
European Railway Agency, as well as in industrial technology transfer
projects. The projects aim at applying research results to key
application domains such as space, avionics, railways, hardware design
and mobile embedded applications.

The Embedded Systems Unit is part of Fondazione Bruno Kessler,
formerly Istituto Trentino di Cultura, a public research institute of
the Autonomous Province of Trento (Italy), founded in 1976. The
institute, through its center for the scientific and technological
research, is active in the areas of Information Technology,
Microsystems, and Physical Chemistry of Surfaces and
Interfaces. Today, FBK is an internationally recognized research
institute, collaborating with industries, universities, and public and
private laboratories in Italy and abroad. The institute's applied and
basic research activities aim at resolving real-world problems, driven
by the need for technological innovation in society and industry.

Location
========

Trento is a lively town of about 100.000 inhabitants, located 130 km
south of the border between Italy and Austria. It is well known for
the beauty of its mountains and lakes, and it offers the possibility
to practice a wide range of sports. Trento enjoys a rich cultural and
historical heritage, and it is the ideal starting point for day trips
to famous towns such as Venice or Verona, as well as to enjoy great
naturalistic journeys. Detailed information about Trento and its
region can be found at http://www.trentino.to/home/index.html?_lang=en.

Contact Person
==============

* Alessandro Cimatti
mailto: <cimatti[at]fbk[dot]eu>
http://es.fbk.eu/people/cimatti

最近太忙了 每天回家都夜里了 早上又走...

我看到会发到这里的

Post by shatter;3102222
LZ终于再次冒泡了，这次信息量不少呀，赞一个。

另外麻烦楼主帮忙留意一下information systems方向的PHD信息。谢谢先。

OPEN PHD POSITION: Adaptive Security for Ambient Technology
[ http://mcs.open.ac.uk/jj2924/ambientsec ]

Software Engineering and Design / Human-Centered Computing Groups
Computing Department, The Open University, UK

* Studentship covers all fees and monthly stipend.

The Open University (OU) maintains a highly regarded research base at its central headquarters in Milton Keynes (near London and within one hour from Cambridge and Oxford). The Computing Department is part of the Computing Research Centre. The Software Engineering and Design research group in the Department has a world class research record and reputation in requirements and security engineering; software architecture, design and evolution; automated software engineering; and empirical studies of software development. The Human-Centered Computing research group is an international leader in human-centred computing, working on new frameworks, methods and approaches for studying and supporting people using mobile, ubiquitous and web-based computing technologies in a way that goes beyond the old HCI paradigm.

The PhD project will benefit from the Laboratory for Ambient and Ubiquitous Technologies that will be housed in purpose built facilities from May 2008, and will interact with existing, externally funded research projects, such as:

   * PRiMMA: Privacy Rights Management for Mobile Applications (funded by EPSRC, in cooperation with IBM Research, Imperial College London and others)
   * Verifying Implementations of Security Protocols in C (funded by and in cooperation with Microsoft Research Cambridge)
   * Royal Society Joint International Project on "Relating Security Requirements and Design" with National Institute for Informatics (Tokyo, Japan)
   * Royal Society Joint International Project on model-based security analysis with TU Munich (Germany)

The PhD Studentship will investigate "Adaptive Security for Ambient Technology (AmbientSec)". The goal is to develop techniques and tools that ensure continuing compliance to security requirements for pervasive systems. More specifically, the focus is on pervasive system devices and their interfaces such as used in modern office environments, and to investigate security issues that may arise in such environments, and how these might be dealt with using available security technology. In particular, the aim is to investigate the notion of "adaptive security" in this context. This will include, for example, questions such as whether security mechanisms may have to adapt to the exact location of an individual in an office building (in the sense of "context-dependent" or "location-based" security).
We will also consider an extension to the more general scenario of a "virtual office" where people are not necessarily in one physical location but may do their office work e.g. while travelling around. A central focus of this work will be the pervasive interfaces between the human users and the computers, on how to integrate these with the adaptive security mechanisms in a secure way, and to evaluate the efficacy and social acceptability of deploying adaptive security measures in situ.

The PhD project is jointly supervised by Jan Jürjens, Bashar Nuseibeh, and Yvonne Rogers. Informal enquiries to any of the PhD supervisors are welcome and encouraged. Contact details can be found at the web-site given below.

The start date of the studentship is 1 Oct. 2008. The award will run for 3 years and includes no teaching obligations.

The applicant should have (or expect to have by the start of the scholarship) a good Masters level degree (or comparable) in Computing, Mathematics, or a related field. Experience or strong interest in one or more of the areas of ubiquitous or pervasive systems or IT security would be an advantage.

Applications submitted by 30 April 2008 will receive full consideration. Details on what the application should include, as well as the address to which it should be submitted (as well as more details about the project), are given at:
http://mcs.open.ac.uk/jj2924/ambientsec

Disabled applicants who meet the essential job requirements will be interviewed.  Further particulars are available in large print, disk or audiotape (minicom 01908 654901). The Open University promotes diversity in employment and welcomes applications from all sections of the community.

Postdoc Position in Formal Methods for Systems-on-a-Chip
========================================================

This announce is also avalaible here:
http://www-verimag.imag.fr/~maraninx/?breve6

====================================================================

Laboratory: VERIMAG Grenoble, France
(VERIMAG is an academic research laboratory affiliated with: the scientific University of Grenoble (UJF), the National Research Center (CNRS) and Grenoble Polytechnic Institute (INPG).
See http://www-verimag.imag.fr/

Group: Synchrone (see ttp://www-verimag.imag.fr/SYNCHRONE)
Collaborations with STMicroelectronics, Grenoble.

1 year, starting after july 08. Possibility of extension.
deadline: may 30, 2008


********************************************************************
***** Context: Transaction-Level Modeling of Systems-on-a-Chip *****
********************************************************************

The Register Transfer Level (RTL) used to be the entry point of the design flow of hardware systems, including systems-on-a-chip (SoCs). However, the simulation environments for such models do not scale up well. Developing and debugging embedded software for these low level models before getting the physical chip from the factory is no longer possible at a reasonable cost. New abstraction levels, such as the Transaction-Level Modeling, have emerged. The TLM approach uses a component-based approach, in which hardware blocks are modules communicating with so-called transactions. The TLM models are used for early development of the embedded software, because the high level of abstraction allows a fast simulation. This new abstraction level requires that SoCs be described in some non-deterministic asynchronous way, with new synchronization mechanisms, quite different from the implicit synchronization of synchronous circuit descriptions.

SystemC is a C++ library used for the description of SoCs at different levels of abstraction, from cycle accurate to purely functional models. It comes with a simulation environment, and is becoming a de facto standard. SystemC offers a set of primitives for the description of parallel activities representing the physical parallelism of the hardware blocks. The TLM level of abstraction can be described with SystemC.


**********************************************************
***** VERIMAG and STMicroelectronics Common Projects *****
**********************************************************

VERIMAG and STMicroelectronics have been working together on TLM-related problems since 2002. The main problems we are looking at are the following:

- How to connect SystemC to formal verification tools; this relies on a front-end for SystemC called PINAPA, and on a semantic extractor able to transform abstract syntax trees of SystemC models into some format suitable for model-checking or abstract interpretation tools.

- How to cover correctly the potential parallelism that is present in a SystemC design, and that is supposed to represent faithfully the physical parallelism of the hardware? Our tool relies on dynamic partial order reduction techniques.

- How to define precisely the nature of the information that should be present in pure functional models (also called TLM-PV, for "programmer’s view") and in timed models (also called TLM-PVT, for "programmer’s view + time)? How to construct a PVT model from a PV one without modifying its functionality, as seen by the developer of the embedded software?

- How to define precisely what a TLM component should be, be it written in SystemC or not?

These questions are being addressed in several projects:
- openTLM is a project of the competitiveness pole MINALOGIC in Grenoble
- FoToVP (Formal Tools for the Virtual Prototyping of Embedded Systems) is a French National Project

Applying formal validation techniques to SystemC descriptions of SoCs requires that the semantics of the language be formalized. The model of time and concurrency underlying the SystemC definition is intermediate between pure synchrony and pure asynchrony. We already experimented three ways of formalizing the semantics: 1) by an encoding into a synchronous formalism; 2) by an encoding into an asynchronous formalism; 3) by the definition of an ad-hoc product.

All these approaches rely on the use of a formally defined intermediate formalism, between SystemC and the available verification tools (models-checkers, abstract-interpretation tools). The format we have now is called HPIOM (for Heterogeneous Parallel Input Output Machines). It is made of interpreted automata, composed with a simple synchronous product.

**********************
***** Objectives *****
**********************

The main result expected from the postdoctoral position is the definition of a new intermediate format, adapted from HPIOM, able to take into account several aspects that have appeared to be important when trying to exploit verification tools from HPIOM. The new format should be more modular than HPIOM, to be able to exploit the modular structure of SystemC/TLM designs; it should allow to mix synchronous and asynchronous behaviors in an explicit way (for the moment asynchronous aspects are encoded into the synchronous framework); finally it should be possible to control the granularity of the behaviors. The definition of this format will need in depth bibliographic work. In order to define this new formalism, it will be necessary to have a look at the existing front-end.

***************************
***** Required Skills *****
***************************

The ideal candidate should have a Ph.D degree in computer science, combine solid theoretical background and software development skills, and have some degree of autonomy. Good English speaking and writing skills are required (French is not required). The candidate should be able to work in a collaborative environment, with a strong commitment to reaching research excellence and achieving assigned objectives.

In depth previous experience in the following areas is required:
- C++ (some knowledge of SystemC would be appreciated)
- Formal languages, automata, compilation, semantics of programming languages

*******************************
***** Terms of employment *****
*******************************

A fulltime position as a postdoctoral researcher for an initial period of 12 months starting as soon as possible after July 1, 2008. The position can be extended to 12 more months.

The salary will be min. 2500 EUR and max 3000 EUR gross per month depending on qualifications and experience.


***********************
***** Application *****
***********************

Send a detailed CV, a list of publications, a list of referees (persons that can recommend you), and a short letter explaining your motivations for this position, by email to:

Florence.Maraninchi@imag.fr,Matthieu.Moy@imag.fr

Please include [POSTDOC SOC] in the subject of your mail, and only attach PDF files.

Deadline: May 30, 2008

Uppsala University, Sweden

Department of Information Technology,

Chair in Embedded Systems

The Department of Information Technology, Uppsala University, invites
applications for a Position as Chaired Professor in the area of Embedded
Systems. The focus of the position is on embedded systems design, especially
concerning aspects of relevance for software. The successful candidate will
develop and lead a strong program of research and teaching on embedded
systems.
The position is placed in the Division of Computer Systems.
Research at the division include computer architecture, computer networks,
real time and embedded systems, formal specification and verification, and
pedagogic methods for computer science education. More information at
http://www.it.uu.se/research/docs.

We expect strong candidates to have an excellent scientific track record,
leadership and management qualities, a strong vision on future development of
the field, and very good teaching skills.

Application Deadline: May 20. Women are especially invited to apply.
More information on the application procedure at
http://www.personalavd.uu.se/ledigaplatser/755prof_eng.html

The Institute for Correct System Design, The University of Oldenburg,
Germany, currently offers several

PhD positions in the area of Computer Security Foundations.

Please find a brief description of the PhD topics below. The positions
are funded by the Graduate School Trustworthy Software Systems. For
information on how to apply please refer to

http://www.uni-oldenburg.de/trustsoft/en/31401.html


Analysis of Security APIs (Froeschle)

A security API is an application programmer's interface that enforces a
security policy on the access and management of sensitive data such as
cryptographic keys. Such APIs form the top level software component of
hardware security modules (HSMs). HSMs are tamper-resistant
cryptoprocessors; for example they are employed by banks to protect the
PINs that allow users of ATMs to identify themselves. In 2000 researchers
of Cambridge University discovered that HSMs can be compromised by
logical flaws in the security APIs: it was demonstrated how an
attacker can trick an HSM into revealing a secret by feeding it a valid
but unexpected sequence of commands. API attacks remain poorly understood,
and it is a topic of ongoing research of how to safeguard against them.
In particular, researchers have started to explore methods for the formal
analysis of security APIs, building on the established techniques for
security protocols. It is the goal of this PhD project to contribute
to this line of research.

Communication and Security in Advanced Messaging Middleware (Froeschle)

Middleware is the enabling technology for distributed software
systems, in which disparate components communicate via heterogenous
networks: middleware software makes the complexity of the underlying
communication transparent for the participating components.
Messaging middleware is not based on the usual procedure- or function
calls but works via the exchange of messages. Typically the messaging
is asynchronous and makes use of the concept of message queuing.
There is a trend that next-generation messaging middleware will be more
'advanced' in that it will take over functionality that is currently
provided externally, for example security mechanisms such as authentication.
Part of this trend is the Advanced Message Queuing Protocol (AMQP),
a platform-independent open standard for messaging middleware, which is
currently under development by a group of companies. Advanced messaging
middleware will on the one hand be more error-prone while at the same
time it must be trustworthy. Therefore, the goal of this PhD project
is to develop a framework that is particularly suited to the formal
analysis of such software. The starting point is provided by the
process calculi for mobile processes such as the pi-calculus as well as
by those formalisms used in the area of security protocols. There are
good contacts to the AMQP project group and hence there is the chance
that the results of the PhD will influence the standard.

Verification and implementation of security automata (Olderog)

Security automata were suggested by Schneider as an abstract mechanism
to characterize and specify security policies that can be enforced by
monitoring system execution. Basin, Olderog, and Sevinc showed that
security automata and their combination with target systems can well be
specified in CSP-OZ, an integration of Communicating Sequential
Processes (CSP) and Object-Z (OZ). This thesis pursues two aims. First,
it will develop dedicated automatic verification methods that target
systems and security automata together satisfy desired security properties.
Second, it will develop transformational methods for generating code
from the security automata to enforce the security policies in a
concrete security architecture.

---
Sibylle Froeschle
University of Oldenburg
http://csd.informatik.uni-oldenburg.de/~sib
_______________________________________________
Concurrency mailing list
Concurrency@listserver.tue.nl
http://listserver.tue.nl/mailman/listinfo/concurrency

Post-Doc Positions Available

           Automated Support for Service Oriented Applications

               Service-Oriented Applications Research Group
                       Fondazione Bruno Kessler
                             Trento, Italy

Deadline: June 30, 2008


The Service Oriented Applications (SOA) Research Group
(http://soa.fbk.eu), part of the Center for Scientific and
Technological Research (IRST) of the Bruno Kessler Foundation in
Trento, Italy (http://www.fbk.eu/irst), is seeking candidates for
Post-Doc positions.

The activity will be carried out in Trento, and will aim at the design
and development of methodologies and support tools for the automated
integration, and the run-time checking of distributed services. In
particular, the activities will focus on the following topics:
- automated resource-based composition of business processes
- self-adapting service orchestration
- assumption-based service monitoring and adaptation

The activities will be carried out within the European Projects ALLOW,
SCUBE and SLA@SOI of the 7th framework programme.
Detailed information on these projects can be found at
http://soa.fbk.eu/projects.php .

The successful candidates will be enrolled with a fixed length
contract of 3 years, and will be subject to a 6 months trial work
period.


Candidate Profile
=================

The ideal candidate should have a Ph.D degree in computer science,
mathematics or electronic engineering or proved equivalent experience,
combine solid theoretical background and software development skills,
and have some degree of autonomy.

The candidate should be able to work in a collaborative environment,
with a strong commitment to achieving assigned objectives and reaching
research excellence.

In depth previous experience in at least one of the following areas is
required:
- Service-Oriented Architectures
- Enterprise Application Integration
- Automated Planning and Software Synthesis
- Semantic Web Services

Presentation and Inquiries
==========================

Candidates interested in the above positions should introduce
themselves and inquire for further information by sending email to
<jobs[at]fbk[dot]eu>.

Applications should contain a statement of interest, with a Curriculum
Vitae, and three reference persons. PDF format is strongly encouraged.

Emails will be automatically processed and should have

'RIF: SOA/postdoc'

as subject.

The SOA Research Group
======================

Led by Marco Pistore, the Service Oriented Applications Research Group
(http://soa.fbk.eu) consists of about 15 persons, including
researchers, Ph.D., post-Doc, and programmers, doing research in the
field of service oriented computing, web services, and distributed
business processes.

The research of the group focuses in particular on the development of
techniques and tools that enact the effective, reliable, low-cost, and
time-efficient composition and monitoring of distributed business
processes through web service technologies. The pioneering research
performed by the SOA group in this area is widely recognized to be
state-of-the- art for what concerns advanced methodologies and
automated support tools for the design and execution of distributed
web processes. Such results are embedded within the ASTRO platform
(http://www.astroproject.org/), which includes and integrates tools
for service composition, verification, execution, and
monitoring. Current research directions of the unit include user
centric service composition (i.e., the composition and enactment of
available services to fulfill specific requirements of the end-user)
and evolution and adaptation of service compositions through autonomic
mechanisms and aspect-oriented design approaches.

The group is currently involved in several research projects, as well
as in industrial projects aiming at applying the research results of
the group to key application domains such as Telco, e-government,
and logistics.

Location
========

Trento is a lively town of about 100.000 inhabitants, located about 130
km south of the border between Italy and Austria. It is well known for
the beauty of its mountains and lakes, and it offers the possibility
to practice a wide range of sports. Trento enjoys a rich cultural and
historical heritage, and it is the ideal starting point for day trips
to famous towns such as Venice or Verona, as well as to enjoy great
naturalistic journeys. Detailed information about Trento and its
region can be found at http://www.trentino.to/home/index.html?_lang=en .

Contact Person
==============

Marco Pistore
mailto: <pistore[at]fbk[dot]eu>
http://soa.fbk.eu/people/pistore/

The Eindhoven University of Technology (TU/e) has the following two vacancies:

2 PhD Students on “Transformations, Refinements and Abstractions of Embedded System Models” (V35.397 and V32.019)

This is a cooperation between one PhD student at the Systems Engineering (SE) Group, Department of Mechanical Engineering (ME),
and one PhD student at the Formal Methods (FM) Group, Department of Mathematics and Computer Science (CS).

Project The TRANSFORMAL project focuses on the development of transformation, refinement and abstraction features for the Chi language,
with an emphasis on model based design of embedded systems at different levels of abstraction. Mathematical correctness and industrial applicability
will both play an important role in this development.

Work The two PhD-candidates we seek will work together on the development of refinement and abstraction techniques for model based design.
The work of the candidate for the FM Group will have an emphasis on the formal correctness of the developed techniques (developing the techniques right),
while the work of the candidate for the SE Group will have an emphasis on developing and applying the techniques in close cooperation with industry,
based on modeling, simulation and control of actual industrial systems (developing the right techniques).

Requirements

We are looking for two candidates who meet the following requirements:

MSc in Mathematics, Computer Science, Electrical or Mechanical Engineering.
Strong affinity with both dynamical systems modeling and theoretical computer science.
Good communication and writing skills in English.
Appointment and Salary

We offer:

A challenging job in a dynamic and ambitious university.
A full-time employment for 4 years, with an intermediate evaluation after 1 year.
A salary of Euro 2000 per month (gross) in the first year, increasing to Euro 2558 per month (gross) in the fourth year.
Moreover 8% holiday allowance is provided annually.
Assistance for finding accommodation can be given.
Support with your personal development and career planning.
Attractive secondary labour conditions (including excellent work facilities, child care, excellent sport facilities).
Application

If you are interested in this PhD position, please send an email containing a detailed curriculum vitae, an explanation of your interest in the proposed research
topic, a publication list, your course programme and corresponding grades, references and all other information that might be relevant to your application.
Please mention TRANSFORMAL and the vacancy number V35.397 and/or V32.019 in the subject. The email addresses for applications
(and for additional information) are d.a.v.beek@tue.nl (dr.ir. D.A. van Beek, Systems Engineering), and p.j.l.cuijpers@tue.nl (dr.ir. P.J.L. Cuijpers, Formal Methods).

Call for Application to a Three-Years PhD Grant

Reliability and safety of  medical device software systems

October 2008

Laboratory :  The MOSEL research team at  LORIA UMR 7503   Nancy, France.

Supervisor::    MERY Dominique  mery@loria.fr

Summary of the topics

The aim of this project is to investigate  the modelling  of medical device software  and systems  using  formal techniques and using proof assistants.  Classical methods like tests have  reached  their limits and   the development of medical device software and systems is a crucial issue, since   the society  should ensure  safe advances in healthcare delivery.   Any safety and regulatory  requirements for medical devices necessarily call for rigorous software developments methods to ensure  reliability  and to protect the public health.   The Grand Challenge  mentions a very interesting case study, namely   the model of a pacemaker, and   there are a lot of other   systems which are now embedded in our body and require investigations on modelling them. Research directions will    focus on the use of proof-based modelling techniques like RAISE, DC, Event B, .... and intends to study the questions of  validation, certification, maintenance, usability and adaptability.   The work will evaluate the impact of mathematical proofs in the modelling technique and the general approach will  be based on domain engineering and  on model-based approach; we will  found our work on the triptych   Domain, System, Requirement.  The research will involve collaboration with therapists and surgeons.



General Informations

We seek a PhD student with an interest in  modelling, proving and developing.   Modelling will be a very crucial part of the work and students should have  skills in using at least one formal method (RAISE, Z, VDM, B, ...)  or semi-formal method (UML,SYSML? ...). The PhD student should have an effective background in computer science. The language of  work will be either french or english.

Applications are invited for a 3-year PhD studentship starting Autumn 2008 under the  supervision of  Pr Dominique Méry. This project is a collaboration between   the MOSEL team  and the University Hospital  of Nancy.  The student will register for a PhD in the Doctoral School  IAEM (Informatique,Automatique,Electronique,Mathématiques)  of the University Henri Poincaré Nancy 1 Department of Computer Science.



Funding Notes: Salary rate (French Ministry of Education): ca. 19200 euros per year.

Applicants should hold at least a  MSc (or equivalent) in computer science or in computing  science . Informal inquiries can be made to Dominique Mery  (mery@loria.fr).

To apply:  send  an application  by email to Dominique Méry (mery@loria.fr) Subject: Application PhD withy the following items:

·         a detailed cv

·          records of  results and marks  in master and previous years

·          name and email of two referees supporting the application

·         a statement of the last degree

·         any document   for improving the application



Other informations:

·         http://www.loria.fr/~mery/phd

·          Ministère de l'Education Nationale et de la Recherche: http://edges.sup.adc.education.fr/portailthese/resultat_these.php?region=41&secteur=X&theme=X&valider=Ok+>



The closing date is 7 June 2008