WorldCat Identities

Sifakis, J. (Joseph) 1946-

Works: 58 works in 137 publications in 3 languages and 1,944 library holdings
Genres: Conference papers and proceedings 
Roles: Author, Editor, Thesis advisor, Opponent, 956, Honoree, dgs
Publication Timeline
Most widely held works by J Sifakis
Embedded systems design : the ARTIST roadmap for research and development by Bruno Bouyssounouse( )

15 editions published in 2005 in English and held by 610 WorldCat member libraries worldwide

"This book is the result of work in the ARTIST FP[subscript 5] project funded by the European Commission's IST programme. It integrates contributions from 28 leading European research teams including many of the top researchers in the area. It assesses the current state of the art on selected topics in embedded systems design, and proposes useful and challenging directions for future research and development." "This monograph-like book is a valuable source of reference for researchers active in the field, and is an excellent introduction for researchers and engineers interested in embedded systems design."--Jacket
Automatic verification methods for finite state systems : international workshop, Grenoble, France, June 12-14, 1989 : proceedings by J Sifakis( Book )

22 editions published in 1990 in English and Italian and held by 505 WorldCat member libraries worldwide

Embedded software : second international conference, EMSOFT 2002, Grenoble, France, October 7-9, 2002 : proceedings by Alberto Sangiovanni-Vincentelli( Book )

24 editions published between 2002 and 2003 in English and held by 370 WorldCat member libraries worldwide

This book constitutes the refereed proceedings of the Second International Conference on Embedded Software, EMSOFT 2002, held in Grenoble, France in October 2002. The book presents 13 invited papers by leading researchers and 17 revised full papers selected during a competitive round of reviewing. The book spans the whole range of embedded software, including operating systems and middleware, programming languages and compilers, modeling and validation, software engineering and programming methodologies, scheduling and execution-time analysis, formal methods, and communication protocols and fault-tolerance
From programs to systems - the systems perspective in computing : ETAPS Workshop, FPS 2014, in honor of Joseph Sifakis, Grenoble, France, April 6, 2014, proceedings by Saddek Bensalem( )

3 editions published in 2014 in English and held by 334 WorldCat member libraries worldwide

From Programs to Systems - The Systems Perspective in Computing" workshop (FPS 2014) was held in honor of Professor Joseph Sifakis in the framework of the 16th European Joint Conferences on Theory and Practice of Software, ETAPS, in Grenoble, April 2014. Joseph Sifakis is an active and visionary researcher in the area of system design. He believes that endowing design with scientific foundations is at least of equal importance as the quest for scientific truth in natural sciences. Previously, he has worked on Petri nets, concurrent systems, program semantics, verification, embedded systems, real-time systems, and formal methods more generally. This book contains 18 papers covering various topics related to the extension of programming theory to systems
Modèles temporels des systèmes logiques by J Sifakis( Book )

6 editions published between 1974 and 2005 in French and Undetermined and held by 17 WorldCat member libraries worldwide

Special issue on hybrid systems by Amir Pnueli( Book )

2 editions published in 1995 in English and held by 7 WorldCat member libraries worldwide

Rigorous system design by J Sifakis( Book )

2 editions published in 2013 in English and held by 7 WorldCat member libraries worldwide

Conception des systèmes logiques : 2e année ENSIMAG-C'4 maîtrise informatique by Charles Payan( Book )

in French and held by 5 WorldCat member libraries worldwide

Notes et compléments de cours sur les réseaux de Pétri by J Sifakis( Book )

1 edition published in 1982 in French and held by 4 WorldCat member libraries worldwide

Impact des modèles d'exécution pour l'ordonnancement en calcul parallèle by Alfredo Goldman( Book )

3 editions published between 1999 and 2004 in French and held by 4 WorldCat member libraries worldwide

Le contexte général de ce travail est l'étude du comportement d'applications parallèles, représentées par un graphe de précédence. La programmation de telles applications dépend fortement des supports d'exécution. Nous présentons et discutons les principaux modèles d'exécution et leur influence sur les problèmes d'ordonnancement des tâches du programme parallèle. Nous étudions en détail quatre problèmes d'ordonnancement sur des modèles d'exécution où le coût de communication est pris en compte. Nous proposons une solution pour un problème à grain très fin, le problème du sac à dos, sur hypercube dans un modèle d'exécution synchrone où le coût de communication est implicite. Nous étudions l'ordonnancement de chaînes sur un modèle à gros grain de communication, le modèle BSP. Nous démontrons qu'ici la recherche d'un ordonnancement optimal est un problème NP-difficile. Nous proposons des solutions avec un compromis entre le nombre de phases de communication/synchronisation et le temps d'inactivité dans chaque processeur. Les deux derniers problèmes étudiés concernent des techniques qui permettent de réduire l'impact du coût des communications inter processeurs. La première technique considère la duplication des tâches. Nous proposons un algorithme de liste avec garantie de performance 2 pour les problèmes à petit temps de communication sur un nombre limité de processeurs. Le deuxième méthode consiste à optimiser les phases de communication en ordonnançant les transmissions de messages. La recherche de la solution optimale étant NP-difficile, nous proposons plusieurs heuristiques
Logiques du temps arborescent pour la spécification et la preuve de programmes by Susanne Graf( Book )

1 edition published in 1984 in French and held by 4 WorldCat member libraries worldwide

Nous étudions les logiques du temps arborescent en tant qu'outils de spécification et de preuve des programmes. Les différentes logiques modales et temporelles sont comparées par rapport aux deux critères suivantes: puissance d'expression et décidabilité. Cette étude porte essentiellement sur fa comparaison des logiques du temps arborescent et des logiques du temps linéaire. Ensuite, le problème de l'utilisation des logiques du temps arborescent en tant qu'outils de preuves des programmes est étudié. Nous proposons une logique pour la preuve constructive des propriétés des processus contrôlables de CCS. Cette logique est telle, que la relation de congruence induite est la congruence observationnelle de CCS
Logics and Models of Concurrent Systems (Volume 13) by EM Clarke( )

3 editions published in 1985 in English and Undetermined and held by 3 WorldCat member libraries worldwide

Distributed Implementations of Component-based Systems with Prioritized Multiparty Interactions : Application to the BIP Framework. by Jean Quilbeuf( )


Distributed software is often required for new systems, because of efficiency and physical distribution and sensors and actuators. Ensuring correctness of a distributed implementation is hard due to the interleaving of actions belonging to distinct processes. This thesis proposes a method for generating a correct and efficient distributed implementation from a high-level model of an application. The input model is described as a set of components communicating through prioritized multiparty interactions. Such primitives change the state of all components involved in an interaction during a single atomic execution step. We assume that a distributed implementation is a set of processes communicating through asynchronous message-passing. The main challenge is to produce a correct and efficient distributed implementation of prioritized multiparty interactions, relying only on message-passing. The method relies on a rigorous design flow refining the high-level model of the application into a low-level model, from which code for a given platform is generated. All intermediate models appearing in the flow are expressed using the same semantics as the input model. Complex interactions are replaced with constructs using simpler interactions at each step of the design flow. In particular, the last model obtained before code generation contains only interactions modeling asynchronous message passing. The correctness of the implementation is obtained by construction. Using multiparty interaction reduces drastically the set of reachable states, compared to an equivalent model expressed with lower level primitives. Essential properties of the system are checked at this abstraction level. Each transformation of the design flow is simple enough to be fully formalized and proved by showing observational equivalence or trace equivalence between the input and output models. The obtained implementation is correct with respect to the original model, which avoids an expensive a posteriori verification. Performance can be optimized through adequate choice of the transformation parameters, or by augmenting the knowledge of components. The latter solution requires to analyze the original model to compute the knowledge, that is reused at subsequent steps of the decentralization. The various transformations and optimizations constituting the design flow have been implemented using the BIP framework. The implementation has been used to evaluate the different possibilities, as well the influence of parameters of the design flow, on several examples. The generated code uses either Unix sockets, MPI or pthreads primitives for communication between processes
QUASAR : une réalisation du système CESAR : description, spécification et analyse des applications réparties by Jean-Philippe Schwartz( )

1 edition published in 1983 in French and held by 3 WorldCat member libraries worldwide

Cette thèse porte sur la réalisation d'une maquette du système CESAR, système d'aide à l'analyse d'applications réparties. L'outil réalisé permet de comparer une application décrite par un programme parallèle avec ses spécifications données par un ensemble de formules d'une logique temporelle
Implémentation rigoureuse des systèmes temps-réels by Tesnim Abdellatif( )

1 edition published in 2012 in French and held by 3 WorldCat member libraries worldwide

Context: Real-time systems are systems that are subject to "real-time constraints"- e.g. operational deadlines from event to system response. Often real-time response times are understood to be in the order of milliseconds and sometimes microseconds. Building real-time systems requires the use of design and implementation methodologies that ensure the property of meeting timing constraints e.g. a system has to react within user-defined bounds such as deadlines and periodicity. A missed deadline in hard real-time systems is catastrophic, like for example in automotive systems, for example if an airbag is fined too late in a car accident, even one ms too late leads to serious repercussions. In soft real-time systems it can lead to a significant loss of performance and QoS like for example in networked multimedia systems. Contribution: We provide a rigorous design and implementation method for the implementation of real-time systems. The implementation is generated from a given real-time application software and a target platform by using two models: * An abstract model representing the behavior of real-time software as a timed automaton. The latter describes user-defined platform-independent timing constraints. Its transitions are timeless and correspond to the execution of statements of the real-time software. * A physical model representing the behavior of the real-time software running on a given platform. It is obtained by assigning execution times to the transitions of the abstract model. A necessary condition for implementability is time-safety, that is, any (timed) execution sequence of the physical model is also an execution sequence of the abstract model. Time-safety means that the platform is fast enough to meet the timing requirements. As execution times of actions are not known exactly, time-safety is checked for worst-case execution times of actions by making an assumption of time-robustness: time-safety is preserved when speed of the execution platform increases. For given real-time software and execution platform corresponding to a time-robust model, we define an execution Engine that coordinates the execution of the application software so as to meet its timing constraints. Furthermore, in case of non-robustness, the execution Engine can detect violations of time-safety and stop execution. We have implemented the execution Engine for BIP programs with real-time constraints. We have validated the method for the design and implementation of the Dala rover robot. We show the benefits obtained in terms of CPU utilization and amelioration in the latency of reaction
ALDEBARAN un système de vérification par réduction de processus communicants by Jean-Claude Fernandez( Book )

2 editions published between 1988 and 2008 in French and held by 3 WorldCat member libraries worldwide

Le système de vérification propose permet de réduire et de comparer des systèmes de transitions étiquetées en tenant compte d'une relation d'équivalence. Les relations d'équivalence considérées sont la congruence forte, l'équivalence et la congruence observationnelles et la congruence par modèle d'acceptation. Les bases théoriques d'Aldebaran sont présentées ainsi que des algorithmes efficaces pour la comparaison et les réductions de systèmes de transition étiquetées et une réalisation en langage C
Comparaison des comportements des processus communicants : application au langage FP2 by S Roge( )

2 editions published between 1986 and 2008 in French and held by 3 WorldCat member libraries worldwide

Dans un premier temps, nous présentons des modèles permettant de décrire des systèmes de processus communicants, synchronisés par rendez-vous, ainsi que les différentes théories qui traitent le problème de la comparaison observationnelle. Nous abordons ensuite le problème à partir du langage FP2. Nous proposons une démarche qui permet de faire totalement abstraction des événements internes des processus et d'exprimer le comportement de communication des processus en n'utilisant que les événements de communication avec l'environnement. Enfin, une notion de contexte est définie et étudiée
Spécification et validation de systèmes en Xesar by Conxita Rodriguez( Book )

2 editions published between 1988 and 2008 in French and English and held by 3 WorldCat member libraries worldwide

Étude de méthodes de spécification et vérification des protocoles de communication. La méthode de vérification mise en œuvre consiste a évaluer les spécifications du protocole sur un modèle fini qui le représente. Le langage de spécification est basé sur un mu calcul permettant l'expression aussi bien de comportements que de propriétés
Contribution à l'étude d'un agent rationnel : spécification en logique intensionnelle et implantation by J.-P Muller( Book )

1 edition published in 1987 in French and held by 3 WorldCat member libraries worldwide

Cette étude porte sur l'architecture globale d'un agent rationnel. Le terme agent est donne aux systèmes autonomes, c'est a dire capables d'agir sans intervention extérieure. De plus, l'hypothèse qu'il est rationnel est faite, c'est a dire que l'ensemble de ses activités extérieures, perceptives et déductives sont justifiables par ses buts. La spécification et l'implantation sont décrites
Verification of Weakly-Hard Requirements on Quasi-Synchronous Systems by Gideon Smeding( )

1 edition published in 2013 in English and held by 3 WorldCat member libraries worldwide

The synchronous approach to reactive systems, where time evolves by globally synchronized discrete steps, has proven successful for the design of safetycriticalembedded systems. Synchronous systems are often distributed overasynchronous architectures for reasons of performance or physical constraintsof the application. Such distributions typically require communication and synchronizationprotocols to preserve the synchronous semantics. In practice, protocolsoften have a significant overhead that may conflict with design constraintssuch as maximum available buffer space, minimum reaction time, and robustness.The quasi-synchronous approach considers independently clocked, synchronouscomponents that interact via communication-by-sampling or FIFO channels. Insuch systems we can move from total synchrony, where all clocks tick simultaneously,to global asynchrony by relaxing constraints on the clocks and withoutadditional protocols. Relaxing the constraints adds different behaviors dependingon the interleavings of clock ticks. In the case of data-flow systems, onebehavior is different from another when the values and timing of items in a flowof one behavior differ from the values and timing of items in the same flow ofthe other behavior. In many systems, such as distributed control systems, theoccasional difference is acceptable as long as the frequency of such differencesis bounded. We suppose hard bounds on the frequency of deviating items in aflow with, what we call, weakly-hard requirements, e.g., the maximum numberdeviations out of a given number of consecutive items.We define relative drift bounds on pairs of recurring events such as clockticks, the occurrence of a difference or the arrival of a message. Drift boundsexpress constraints on the stability of clocks, e.g., at least two ticks of one perthree consecutive ticks of the other. Drift bounds also describe weakly-hardrequirements. This thesis presents analyses to verify weakly-hard requirementsand infer weakly-hard properties of basic synchronous data-flow programs withasynchronous communication-by-sampling when executed with clocks describedby drift bounds. Moreover, we use drift bounds as an abstraction in a performanceanalysis of stream processing systems based on FIFO-channels
moreShow More Titles
fewerShow Fewer Titles
Audience Level
Audience Level
  Kids General Special  
Audience level: 0.64 (from 0.53 for From progr ... to 0.96 for Distribute ...)

Embedded systems design : the ARTIST roadmap for research and development
Automatic verification methods for finite state systems : international workshop, Grenoble, France, June 12-14, 1989 : proceedingsEmbedded software : second international conference, EMSOFT 2002, Grenoble, France, October 7-9, 2002 : proceedings
Alternative Names
Iosif Sifakis

Joseph Sifakis

Joseph Sifakis chercheur en informatique français d'origine grecque

Joseph Sifakis Frans informaticus

Joseph Sifakis fransk ingeniør og informatikar

Joseph Sifakis fransk ingeniør og informatiker

Joseph Sifakis fransk ingenjör och datavetare

Joseph Sifakis Greek-French computer scientist

Joseph Sifakis griechisch-französischer Informatiker

Joseph Sifakis informàtic francès d'origen grec

Joseph Sifakis informático francés de origen griego

Joseph Sifakis informatico greco

Sifakis, J.

Sifakis, J. 1946-

Sifakis, Joseph

Sifakis, Joseph 1946-

Ιωσήφ Σηφάκης

Σηφάκης, Ιωσήφ 1946-

Йосиф Сіфакіс

Сифакис, Иосиф

جوزف سیفاکیس

جوزف سیفاکیس دانشمند علوم کامپیوتر و مهندس فرانسوی

جوزيف سيفاكيس



English (71)

French (22)

Italian (1)