Email Gateway (Aug 18 2022 at 12:14): Email Gateway (Aug 18 2022 at 12:14):From: "julien@RadboudUniversity" <julien@cs.ru.nl>
[ We apologize if you received multiple copies of this message. ]
PhD Position on Formal Verification of Deadlock Avoidance Mechanisms
in NoCs
The Informatics for Technical Applications group at the Radboud
University Nijmegen invites applications for a PhD position in the
context of the NWO project "Formal Verification of Deadlock Avoidance
Mechanisms" (see http://www.cs.ru.nl/~julien/Julien%20at%20Nijmegen/
FVDAM.html).
The Radboud University Nijmegen is one of the leading academic
communities in the Netherlands. Renowned for its green campus, modern
buildings, and state-of-the-art equipment, it has nine faculties and
enrolls over 17.500 students in approximately 90 study programs. The
university is situated in the oldest Dutch city, close to the German
border, on the banks of the river Waal (a branch of the Rhine). The
city has a rich history and one of the liveliest city centers in the
Netherlands.
The Informatics for Technical Applications (ITA) group is part of the
Institute for Computing and Information Sciences (ICIS). The group
develops formal methods and tools for the specification, design,
analysis and testing of embedded systems, distributed algorithms and
protocols, and assesses and demonstrates the effectiveness of these
methods and tools in the industrial development process. ITA has an
excellent international reputation and its research program was
singled out as "Excellent" in the last national research assessment.
Project Description
Network-on-chip is an emerging paradigm that could meet future
applications demand. The correctness of a system-on-chip will largely
depend on the correctness of the NoC. There has been little work on
the application of formal verification techniques to NoCs. This is a
challenging area, in particular, due to fact that the verification
needs to be done on parameterized networks.
The goal of this project is to develop formal verification methods
for parameterized networks on a chip (NoCs). We aim at a general
model and verification methodology that encompasses the essential
constituents of NoCs communication architectures -- that is,
protocols and topologies, routing algorithms, and scheduling policies
-- and applies to a wide variety of systems. The project will tackle
the specification of properties about the absence of deadlock,
livelock, and will allow to quantify the routing performance of an
NoC. In particular, the project will focus on deadlock avoidance
mechanisms. Deadlocks may be generated at the protocol or at the
structural (for example, routing algorithms) level. The challenge of
the project lies in supporting the analysis of these two kinds of
deadlocks for parameterized, or unbounded, models.
To begin with, we want to analyze practical case studies, either
publicly available or provided by industrial partners. Our
methodology will be based on the Generic Network model (GeNoC) and
its implementation in the ACL2 logic. From this practical
experiments, we plan to generalize our approach to generate ranking
function for parameterized systems. One interesting research
direction is to combine the general formalization in ACL2 with
powerful tools dedicated to termination proof, like Terminator.
Requirements
The candidate must hold an MSc or equivalent with top performance in
a field that is closely related to computer science or mathematics.
He or she should have interest in conducting original scientific
research, publishing the results in top conferences and scientific
journals, and participating in teaching duties. Maturity, self-
motivation and the ability to work both independently and as a team
player in local and international research teams are expected. Dutch
language skills are not required, English is mandatory.
Conditions of employment
The positions involve a normal employment contract for a period of up
to 4 years, and is expected to lead to a Ph.D. degree. The salary
grows to approx. 2500 euro gross per month in the fourth year. For
additional information please see our website (http://
www.ita.cs.ru.nl/) and/or contact Julien Schmaltz:
Phone: +31 (0)24-3652104
E-mail: julien - at - cs - dot - ru - dot - nl
Applicants
should submit their application to pz@science.ru.nl or via surface
mail to
Radboud University Nijmegen
Faculty of Science
P&O Department
Attn. Drs. D. Reinders
PO Box 9010
6500 GL Nijmegen
The Netherlands
referring to number 62.69.08.
Applications should include a cover letter, a curriculum vitae, and
contact details of at least 2 references.
Review of completed applications will begin October 1st, 2008. The
position remains open until filled.
Dr. Julien Schmaltz
Model Based System Development (MBSD)
Institute For Computing and Information Sciences
Radboud University Nijmegen
The Netherlands
julien@cs.ru.nl --- www.cs.ru.nl/~julien/
Phone: +31 24 36 52104 --- Fax: +31 24 365 2728
Last updated: May 03 2024 at 08:18 UTC