On the Complexity of Verification-Driven Execution ∗ (2009)
David Harel, Hillel Kugler, Shahar Maoz, Itai Segall
Smart play-out is a method for executing declarative scenario-based requirements, which utilizes powerful model-checking or planning algorithms to run the scenarios and avoid some of the violations...
How avionics work led to a graphical language for reactive systems where the diagrams themselves define the system’s behavior.
Can Programming Be Liberated, Period? (2009)
The author describes his dream about freeing ourselves from the straightjackets of programming, making the process of getting computers to do what we want intuitive, natural, and also fun. He...
Predicting the Receptive Range of Olfactory (2009)
Rafi Haddad, Liran Carmel, Noam Sobel, David Harel
Although the family of genes encoding for olfactory receptors was identified more than 15 years ago, the difficulty of functionally expressing these receptors in an heterologous system has, with only...
Algorithmic Bioprocesses (2009)
Condon, Anne, Harel, David, Kok, Joost, Salomaa, Arto, Winfree, Erik
Some Results on the Expressive Power and Complexity of LSCs ⋆ (2009)
David Harel, Shahar Maoz, Itai Segall
with deep admiration and respect. Abstract. We survey some of the main results regarding the complexity and expressive power of Live Sequence Charts (LSCs). We first describe the two main semantics...
This paper presents a game-model of a gym training system, where the behavior of the system is specified using languages developed originally for reactive system design, which drive a game engine....
Object Composition in Scenario-Based Programming ⋆ (2009)
Yoram Atir, David Harel, Asaf Kleinbort, Shahar Maoz
Abstract. We investigate the classical notion of object composition in the framework of scenario-based specification and programming. We concentrate on live sequence charts (LSC), which extend the...
A metric for odorant comparison (2009)
Rafi Haddad, Rehan Khan, Yuji K Takahashi, Kensaku Mori, David Harel, Noam Sobel
In studies of vision and audition, stimuli can be systematically varied by wavelength and frequency, respectively, but there is no equivalent metric for olfaction. Restricted odorant-feature metrics...
Abstract Visualizing Inter-Dependencies Between Scenarios ∗ (2009)
One of the main challenges in understanding a scenariobased specification of a reactive system is rooted in the inter-dependencies between the scenarios. These are inherently implicit in the very...
David Harel, Shahar Maoz, S. Maoz
from necessary behavior. They thus enable the specification of rich multi-modal scenario-based properties, such as mandatory, possible and forbidden scenarios. The sequence diagrams of UML 2.0 enrich...
Statecharts in the Making: A Personal Account (2009)
Writing a historical paper about something you yourself are heavily involved in is clearly difficult; the result is bound to be personal and idiosyncratic and might well sound presumptuous. The...
Statecharts in the Making: A Personal Account (2009)
Writing a historical paper about something you yourself are heavily involved in is clearly difficult; the result is bound to be personal and idiosyncratic and might well sound presumptuous. The...
Abstract. In this paper we discuss a useful family of graph drawing algorithms, characterized by their ability to draw graphs in one dimension. We define the spe-cial requirements from such...
L. F. Perrone, F. P. Wiel, J. Liu, B. G. Lawson, D. M. Nicol, R. M. Fujimoto, ...
Systems Biology is aimed at analyzing the behavior and interrelationships of biological systems and is characterized by combining experimentation, theory, and computation. Dedicated to exploring...
Early Stages, Pancreatic Organogenesis, Yaki Setty, Irun R. Cohen, David Harel
The pancreas is an essential organ involved in metabolic and digestive pathways [9]. Thus, modeling pancreatic organogenesis may lead to a better understanding of this process and may reveal new...
One-Dimensional Graph Drawing: Part I — Drawing Graphs by Axis Separation (2008)
Abstract. In this paper we discuss a useful family of graph drawing algorithms, characterized by their ability to draw graphs in one dimension. The most important application of this family seems to...
General Terms: Languages (2008)
i-Logix, Inc. We describe the semantics of statecharts as implemented in the STATEMATE system. This was the first executable semantics defined for the language and has been in use for almost a...
L. F. Perrone, F. P. Wiel, J. Liu, B. G. Lawson, D. M. Nicol, R. M. Fujimoto, ...
Systems Biology is aimed at analyzing the behavior and interrelationships of biological systems and is characterized by combining experimentation, theory, and computation. Dedicated to exploring...
Some Challenges for System Development: Layout, Olfaction and Reactive Animation (2008)
This series of lectures will revolve around three topics that are seemingly peripheral to the ”classical ” notion of system development. Here are brief summaries of these, followed by some...
Science From Play-In Scenarios to Code: (2008)
David Harel, The Weizmann, An Achievable Dream
A development scheme for complex reactive systems leads from a userfriendly requirements capture method, called play-in scenarios, to full behavioral descriptions of system parts, and from there to...
A metric for odorant comparison (2008)
Rafi Haddad, Rehan Khan, Yuji K Takahashi, Kensaku Mori, David Harel, Noam Sobel
Modal Semantics for UML Sequence Diagrams (2008)
David Harel, Shahar Maoz, David Harel, Shahar Maoz
Abstract Live Sequence Charts (LSC) extend Message Sequence Charts (MSC), mainly by distinguishing possible from necessary behavior. They thus enable the specification of rich multi-modal...
Evelyn Fox Keller, David Harel
This paper is a response to the increasing difficulty biologists find in agreeing upon a definition of the gene, and indeed, the increasing disarray in which that concept finds itself. After briefly...
Avital Sadot, Jasmin Fisher, Dan Barak, Yishai Admanit, Michael J. Stern, E. Jane, ...
Abstract-- The last several decades have witnessed a vast accumulation of biological data and data analysis. Many of these data sets represent only a small fraction of the system’s behavior, making...
Sol Efroni, David Harel, Irun R. Cohen
One of the problems biologists face is a data set too large to comprehend in full. Experimenters generate data at an ever-growing pace, each from their own niche of interest. Current theories are...
Predicting the Receptive Range of Olfactory Receptors (2008)
Rafi Haddad, Liran Carmel, Noam Sobel, David Harel
Although the family of genes encoding for olfactory receptors was identified more than 15 years ago, the difficulty of functionally expressing these receptors in an heterologous system has, with only...
On Predicting Responses to Mixtures in Quartz Microbalance (2008)
Sensors Liran Carmel, Liran Carmel, Noa Sever, David Harel
A fundamental question in studying odor patterns in electronic noses is how to estimate the response to a mixture, given the response curves of the pure chemicals. We study this question by proposing...
Generic Reactive Animation: Realistic Modeling of Complex Natural Systems (2008)
Abstract. Natural systems, such as organs and organisms, are largescale complex systems with numerous elements and interactions. Modeling such systems can lead to better understanding thereof and may...
Prediction Models for the Pleasantness of Binary Mixtures in Olfaction (2008)
Hadas Lapid, David Harel, Noam Sobel
Whereas the rules underlying the perceived intensity of binary mixtures have been investigated, minimal efforts have been directed at elucidating the rules underlying the perceived pleasantness of...
Prediction Models for the Pleasantness of Binary Mixtures in Olfaction (2008)
Lapid, Hadas, Harel, David, Sobel, Noam
Whereas the rules underlying the perceived intensity of binary mixtures have been investigated, minimal efforts have been directed at elucidating the rules underlying the perceived pleasantness of...
Development of Complex Environment for the Reactive Systems (2007)
David Harel, Hagi Lachover, Amnon Naamad, Amir Pnueli, Michal Politi, Rivi Sherman, ...
Abstract--This paper provides an overview of the STATEMATE ' system, constructed over the past several)ears by the authors and their colleagues at Ad Cad Ltd., the R&D subsidiar.v of...
ABSTRACT Drawing Graphs with Non-Uniform Vertices (2007)
The vertices of most graphs that appear in real applications are nonuniform. They can be circles, ellipses, rectangles, or other geometric elements of varying shapes and sizes. Unfortunately, current...
Communicated by Editor's name Live sequence charts (LSCs) have been defined recently as an extension of message sequence charts (MSCs; or their UML variant, sequence diagrams) for rich...
ABSTRACT Clustering Spatial Data Using Random Walks (2007)
Discovering significant patterns that exist implicitly in huge spatial databases is an important computational task. A common approach to this problem is to use cluster analysis. We propose a novel...
North-Holland STATECHARTS: A VISUAL FORMALISM FOR COMPLEX SYSTEMS* (2007)
David Harel, Communicated A. Pnueli
Abstract. We present a broad extension of the conventional formalism of state machines and state diagrams, that is relevant to the specification and design of complex discrctebevent systems, such as...
North-Holland STATECHARTS: A VISUAL FORMALISM FOR COMPLEX SYSTEMS* (2007)
Abstract. We present a broad extension of the conventional formalism of state machines and state diagrams, that is relevant to the specification and design of complex discrete-event systems, such as...
ABSTRACT Drawing Graphs with Non-Uniform Vertices (2007)
The vertices of most graphs that appear in real applications are nonuniform. They can be circles, ellipses, rectangles, or other geometric elements of varying shapes and sizes. Unfortunately, current...
David Harel, Dexter Kozen, Rohit Parikh
A process logic (PL) is defined that subsumes Pratt's process logic, Parikh's SOAPL, Nishimura's process logic, and Pnueli's Temporal Logic in expressiveness. The language of PL...
Estimating the Size of the Olfactory Repertoire (2007)
Liran Carmel, David Harel, Department Of Molecular Genetics
The concept of shape space, which has been successfully implemented in immunology, is used here to construct a model for the discrimination power of the olfactory system. Using reasonable assumptions...
The STATEMATE Semantics.of (2007)
i-Logix, Inc. We describe the semantics of statecharts as implemented in the STATEMATE system. This was the first executable semantics defined for the language and has been in use for almos'a...
Communicated by Editor's name Live sequence charts (LSCs) have been defined recently as an extension of message sequence charts (MSCs; or their UML variant, sequence diagrams) for rich...
Elsevier Fundamental Study (2007)
Yael Etzion-petruschka, David Harel, Dale Myers
On the solvability of domino snake problems
Drawing Graphs Nicely Using (2007)
The paradigm of simulated annealing is applied to the problem of drawing graphs "nicely." Our algorithm deals with general undirected graphs with straight-line edges, and employs...
ARTICLES ON VISUAL FORMALISMS (2007)
The higraph, a general kind of diagramming object, forms a visual formalism of topological nature. Higraphs are suited for a wide array of applications to databases, knowledge representation, and,...
We describe a programming language IND that generalizes alternating Turing machines to arbitrary first-order structures. We show that IND programs (resp. everywhere-halting IND programs, loop-free...
A High School, Judith Gal-ezer, Catriel Beeri, David Harel, Amiram Yehudai
Computer ience
Article On Folk Theorems (2007)
Criteria are suggested for determining if a statement is a folk theorem. The ideas are then illustrated with a detailed example from the theory of programming.
Executable Object Modeling with (2007)
Statecharts, popular for modeling system behavior in the structural analysis paradigm, are part of a fully executable language set for modeling object-oriented systems. The languages form the core of...
ABSTRACT Smart Play-Out ∗ (2007)
David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli
We describe “smart play-out”, a new method for executing and analyzing scenario based behavior, which is part of the Play-In/Play-Out methodology and the Play-Engine tool. Behavior is “played...
On Mappings Between Electronic Noses (2007)
Oded Shaham, Liran Carmel, David Harel
We consider the task of finding a mapping between two eNoses that employ two different sensor technologies, quartz microbalance and conducting polymers. Such a mapping is a model that predicts the...
Emergent Dynamics of Thymocyte Development and Lineage Determination (2007)
Sol Efroni, David Harel, Irun R. Cohen
Experiments have generated a plethora of data about the genes, molecules, and cells involved in thymocyte development. Here, we use a computer-driven simulation that uses data about thymocyte...
Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based (2007)
Abstract. We introduce a novel approach to the smart execution of scenario-based models of reactive systems, such as those resulting from the multi-modal inter-object language of live sequence charts...
Generic Architecture for Reactive Animation (2007)
This technical report describes in detail a specific mechanism for linking any number of tools, including an animation tool and reactive system engines of different kinds. We illustrate the technique...
Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs (2007)
Abstract. We introduce a novel approach to the smart execution of scenario-based models of reactive systems, such as those resulting from the multi-modal inter-object language of live sequence charts...
Explaining a complex living system: Dynamics, multi-scaling and emergence (2007)
Complex living systems are difficult to understand. They obey the laws of physics and chemistry, but these basic laws do not explain their behaviour; each component part of a complex system...
Emergent dynamics of thymocyte development and lineage determination, PLoS (2007)
Sol Efroni, David Harel, Irun R. Cohen
Experiments have generated a plethora of data about the genes, molecules, and cells involved in thymocyte development. Here, we use a computer-driven simulation that uses data about thymocyte...
S2A: A compiler for multi-modal UML sequence diagrams (2007)
David Harel, Asaf Kleinbort, Shahar Maoz
Abstract. We report on S2A, a compiler that translates Modal UML
Boris Sobolev, David Harel, Christos Vasilakis, Adrian Levy, D. Harel, C. Vasilakis
Abstract Computer simulation of patient flow has been used extensively to assess the impacts of changes in the management of surgical care. However, little research is available on the utility of...
06351 Summary -- Methods for Modelling Software Systems (MMOSS) (2007)
Brinksma, Ed, Harel, David, Mader, Angelika, Stevens, Perdita, Wieringa, Roel
We survey the key objectives and the structure of this Dagstuhl seminar, and discuss common themes that emerged.
06351 Abstracts Collection -- Methods for Modelling Software Systems (MMOSS) (2007)
Brinksma, Ed, Harel, David, Mader, Angelika, Stevens, Perdita, Wieringa, Roel
From 27.08.06 to 01.09.06, the Dagstuhl Seminar 06351 ``Methods for Modelling Software Systems (MMOSS)'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During...
Emergent Dynamics of Thymocyte Development and Lineage Determination (2006)
Sol Efroni, David Harel, Irun R Cohen
Experiments have generated a plethora of data about the genes, molecules, and cells involved in thymocyte development. Here, we use a computer-driven simulation that uses data about thymocyte...
Pierre Combes, David Harel, Hillel Kugler, P. Combes, D. Harel, H. Kugler (b
sequence charts and the Play-Engine tool
David Harel, David Harel, Hillel Kugler, Hillel Kugler, Gera Weiss, Gera Weiss
Abstract. The play-in/play-out approach is a method for specifying and developing complex reactive systems. It is built upon a scenariobased philosophy, and uses the language of live sequence charts...
Temporal logic for scenario-based specifications (2005)
Hillel Kugler, Hillel Kugler, David Harel, David Harel, Amir Pnueli, Amir Pnueli, ...
Abstract. We provide semantics for the powerful scenario-based language of live sequence charts (LSCs). We show how the semantics of live sequence charts can be captured using temporal logic. This is...
Temporal logic for scenario-based specifications (2005)
Hillel Kugler, David Harel, Amir Pnueli, Yuan Lu, Yves Bontemps
Abstract. We provide semantics for the powerful scenario-based language of live sequence charts (LSCs). We show how the semantics of live sequence charts can be captured using temporal logic. This is...
David Harel, Hillel Kugler, Gera Weiss
Abstract. The play-in/play-out approach is a method for specifying and developing complex reactive systems. It is built upon a scenariobased philosophy, and uses the language of live sequence charts...
Synthesis revisited: Generating statechart models from scenario-based requirements (2005)
David Harel, David Harel, Hillel Kugler, Hillel Kugler, Amir Pnueli, Amir Pnueli
Abstract. Constructing a program from a specification is a long-known general and fundamental problem. Besides its theoretical interest, this question also has practical implications, since finding...
Synthesis revisited: Generating statechart models from scenario-based requirements (2005)
David Harel, Hillel Kugler, Amir Pnueli
Abstract. Constructing a program from a specification is a long-known general and fundamental problem. Besides its theoretical interest, this question also has practical implications, since finding...
Pierre Combes, David Harel, Hillel Kugler
Abstract. We apply the language of live sequence charts (LSCs) and the Play-Engine tool to a real-world complex telecommunication service. The service, called Depannage, allows a user to make a phone...
Temporal logic for scenario-based specifications (2005)
Hillel Kugler, David Harel, Amir Pnueli, Yuan Lu, Yves Bontemps
Abstract. We provide semantics for the powerful scenario-based language of live sequence charts (LSCs). We show how the semantics of live sequence charts can be captured using temporal logic. This is...
David Harel, Hillel Kugler, Gera Weiss
Abstract. The play-in/play-out approach is a method for specifying and developing complex reactive systems. It is built upon a scenariobased philosophy, and uses the language of live sequence charts...
Axis-by-Axis Stress Minimization (2004)
Graph drawing algorithms based on minimizing the so-called stress energy strive to place nodes in accordance with target distances. They were first introduced to the graph drawing field by Kamada and...
Smart Play-Out Extended: Time and Forbidden Elements (2004)
David Harel, Hillel Kugler, Amir Pnueli
Smart play-out is a powerful technique for executing live sequence charts (LSCs). It uses verification techniques to help run a program, rather than to prove properties thereof. In this paper we...
Combining Hierarchy and Energy for Drawing Directed Graphs (2004)
Liran Carmel, David Harel, Yehuda Koren
Abstract — We present an algorithm for drawing directed graphs, which is based on rapidly solving a unique onedimensional optimization problem for each of the axes. The algorithm results in a clear...
InterPlay: Horizontal Scale-Up and Transition to Design in Scenario-Based Programming (2004)
Dan Barak, David Harel, Rami Marelly
Abstract. We describe InterPlay, a simulation engine coordinator that supports cooperation and interaction of multiple simulation and execution tools, thus helping to scale-up the design and...
The Rhapsody Semantics of Statecharts (or, On The Executable Core of the UML (2004)
Abstract. We describe the semantics of statecharts as implemented in the current version of the Rhapsody tool. In its original 1996 version this was among the first executable semantics for...
Smart Play-Out Extended: Time and Forbidden Elements (2004)
David Harel Hillel, David Harel, Hillel Kugler, Amir Pnueli
Smart play-out is a powerful technique for executing live sequence charts (LSCs). It uses verification techniques to help run a program, rather than to prove properties thereof. In this paper we...
David Harel, Bernhard Rumpe, Technische Universität Braunschweig
Motivated by the confusion surrounding the proper definition of complex modeling languages, especially the UML, we discuss the distinction between syntax and true semantics, and the nature and...
Combining State-based and Scenario-based Approaches in Modeling Biological Systems (2004)
Jasmin Fisher David, David Harel, E. Jane, Albert Hubbard, Nir Piterman, Michael J. Stern, ...
Biological systems have recently been shown to share many of the properties of reactive systems. This observation has led to the idea of using methods devised for the construction (engineering) of...
Smart Play-Out Extended: Time and Forbidden Elements (2004)
David Harel, David Harel, Hillel Kugler, Hillel Kugler, Amir Pnueli, Amir Pnueli
Smart play-out is a powerful technique for executing live sequence charts (LSCs). It uses verification techniques to help run a program, rather than to prove properties thereof. In this paper we...
Liran Carmel, Noa Sever, David Harel
A fundamental question in studying odor patterns in electronic noses is how to estimate the response to a mixture, given the response curves of the pure chemicals. We study this question by proposing...
The Rhapsody Semantics of Statecharts (or, On The Executable Core of the UML (2004)
Abstract. We describe the semantics of statecharts as implemented in the current version of the Rhapsody tool. In its original 1996 version this was among the first executable semantics for...
Abstract Sensors and Actuators B 106 (2005) 76–82 On mappings between electronic noses (2004)
Oded Shaham, Liran Carmel, David Harel
We consider the task of finding a mapping between two eNoses that employ two different sensor technologies, quartz microbalance and conducting polymers. Such a mapping is a model that predicts the...
A grand challenge for computing: Towards full reactive modeling of a multi-cellular animal (2004)
David Harel, Naaman Kam, Sol Efroni, My Colleagues Michael, Jane Hubbard, Amir Pnueli, ...
challenge is really a direct outcome of our interaction, and many of the points made herein are outcomes of discussions with them. In particular, Naaman Kam deserves special thanks for initiating the...
Combining state-based and scenario-based approaches in modeling biological systems (2004)
Jasmin Fisher, David Harel, E. Jane, Albert Hubbard, Nir Piterman, Michael J. Stern, ...
Abstract. Biological systems have recently been shown to share many of the properties of reactive systems. This observation has led to the idea of using methods devised for the construction...
Formal Modeling of C. elegans Development: A Scenario-Based Approach (2003)
David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli, E. Jane, Albert Hubbard, ...
Summary. We present preliminary results of a new approach to the formal modeling of biological phenomena. The approach stems from the conceptual compatibility of the methods and logic of data...
Message Sequence Charts (2003)
David Harel, P. S. Thiagarajan
Message sequence charts (MSCs) constitute an attractive visual formalism that is widely used to capture system requirements during the early design stages in domains such as telecommunication...
Specifying and Executing Behavioral Requirements: The Play-In/Play-Out Approach (2003)
A powerful methodology for scenario-based specification of reactive systems is described, in which the behavior is “played in ” directly from the system’s GUI or some abstract version thereof,...
Formal Modeling of C. elegans Development: A Scenario-Based Approach (2003)
David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli, E. Jane, Albert Hubbard, ...
Abstract. We present preliminary results of a new approach to the formal modeling of biological phenomena. The approach stems from the conceptual compatibility of the methods and logic of data...
Formal Modeling of C. elegans Development: A Scenario-Based Approach (2003)
David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli, E. Jane, Albert Hubbard, ...
Abstract. We present preliminary results of a new approach to the formal modeling of biological phenomena. The approach stems from the conceptual compatibility of the methods and logic of data...
Axis-by-Axis Stress Minimization (2003)
Yehuda Koren And, Yehuda Koren, David Harel
Graph drawing algorithms based on minimizing the so-called stress energy strive to place nodes in accordance with target distances. They were first introduced to the graph drawing field by Kamada and...
A Two-Way Visualization Method for Clustered Data (2003)
We describe a novel approach to the visualization of hierarchical clustering that superimposes the classical dendrogram over a fully synchronized low-dimensional embedding, thereby gaining the...
Formal Modeling of C. elegans Development: A Scenario-Based Approach (2003)
David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli, E. Jane, Albert Hubbard, ...
Abstract. We present preliminary results of a new approach to the formal modeling of biological phenomena. The approach stems from the conceptual compatibility of the methods and logic of data...
Drawing huge graphs by algebraic multigrid optimization. Multiscale Modeling and Simulation (2003)
Yehuda Koren, Liran Carmel, David Harel
We present an extremely fast graph drawing algorithm for very large graphs, which we term ACE (for Algebraic multigrid Computation of Eigenvectors). ACE exhibits a vast improvement over the fastest...
Drawing huge graphs by algebraic multigrid optimization. Multiscale Modeling and Simulation (2003)
Yehuda Koren, Liran Carmel, David Harel
Abstract. We present an extremely fast graph drawing algorithm for very large graphs, which we term ACE (for Algebraic multigrid Computation of Eigenvectors). ACE exhibits a vast improvement over the...
Efroni, Sol, Harel, David, Cohen, Irun R.
One of the problems biologists face is a data set too large to comprehend in full. Experimenters generate data at an ever-growing pace, each from their own niche of interest. Current theories are...
Graph Drawing by High-Dimensional Embedding (2002)
We present a novel approach to the aesthetic drawing of undirected graphs. The method has two phases: first embed the graph in a very high dimension and then project it into the 2-D plane using...
Drawing Directed Graphs Using One-Dimensional Optimization (2002)
Carmel, Liran, Harel, David, Koren, Yehuda
We present an algorithm for drawing directed graphs, which is based on rapidly solving a unique one-dimensional optimization problem for each of the axes. The algorithm results in a clear description...
Multiple Instances and Symbolic Variables in Executable Sequence Charts (2002)
Rami Marelly, David Harel, Hillel Kugler
submitted for publication. We extend live sequence charts (LSCs), a highly expressive variant of sequence diagrams, and provide the extension with an executable semantics. The extension involves...
Drawing Directed Graphs Using One-Dimensional Optimization (2002)
Liran Carmel, David Harel, Yehuda Koren
We present an algorithm for drawing directed graphs, which is based on rapidly solving a unique one-dimensional optimization problem for each of the axes. The algorithm results in a clear description...
A Multi-scale Algorithm for the Linear Arrangement Problem (2002)
Abstract. Finding a linear ordering of the vertices of a graph is a common problem arising in diverse applications. In this paper we present a linear-time algorithm for this problem, based on the...
Ace: A fast multiscale eigenvectors computation for drawing huge graphs (2002)
Yehuda Koren, Liran Carmel, David Harel
We present an extremely fast graph drawing algorithm for very large graphs, which we term ACE (for Algebraic multigrid Computation of Eigenvectors). ACE finds an optimal drawing by minimizing a...
A Multi-scale Algorithm for the Linear Arrangement Problem (2002)
Abstract. Finding a linear ordering of the vertices of a graph is a common problem arising in diverse applications. In this paper we present a linear-time algorithm for this problem, based on the...
Drawing Directed Graphs Using One-Dimensional Optimization (2002)
Liran Carmel, David Harel, Yehuda Koren
Abstract. We present an algorithm for drawing directed graphs, which is based on rapidly solving a unique one-dimensional optimization problem for each of the axes. The algorithm results in a clear...
Multiple Instances and Symbolic Variables in Executable Sequence Charts (2002)
Rami Marelly, David Harel, Hillel Kugler
We extend live sequence charts (LSCs), a highly expressive variant of sequence diagrams, and provide the extension with an executable semantics. The extension involves support for instances that can...
Ace: A fast multiscale eigenvectors computation for drawing huge graphs (2002)
Yehuda Koren, Liran Carmel, David Harel
We present an extremely fast graph drawing algorithm for very large graphs, which we term ACE (for Algebraic multigrid Computation of Eigenvectors). ACE exhibits an improvement of something like two...
Ace: A fast multiscale eigenvectors computation for drawing huge graphs (2002)
Yehuda Koren, Liran Carmel, David Harel
We present an extremely fast graph drawing algorithm for very large graphs, which we term ACE (for Algebraic multigrid Computation of Eigenvectors). ACE exhibits a vast improvement over the fastest...
Smart play-out of behavioral requirements (2002)
David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli
Abstract. We describe a methodology for executing scenario-based requirements of reactive systems, focusing on "playing-out " the behavior using formal verification techniques for...
A Multi-scale Algorithm for the Linear Arrangement Problem (2002)
Abstract. Linear ordering vertices of a graph is a common problem arising in diverse applications. In this paper we present a novel algorithm for this problem. The algorithm is based on the...
Rhapsody: A Complete Lifecycle Model-Based Development System (2002)
Eran Gery, David Harel, Eldad Palatshy
Model-based development has been a central theme in the software development industry almost since its inception. Nevertheless, model-based development is not yet mainstream practice. The emergence...
Graph drawing by high-dimensional embedding (2002)
Abstract. We present a novel approach to the aesthetic drawing of undirected graphs. The method has two phases: first embed the graph in a very high dimension and then project it into the 2-D plane...
Smart play-out of behavioral requirements (2002)
David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli
Abstract. We describe a methodology for executing scenario-based requirements of reactive systems, focusing on “playing-out ” the behavior using formal verification techniques for driving the...
Playing with time: On the specification and execution of time-enriched LSCs (2002)
Abstract. We extend live sequence charts (LSCs), a highly expressive variant of sequence diagrams, with timing constructs, thus making the language suitable for specifying the behavioral requirements...
On object systems and behavioral inheritance (2002)
Abstract--We consider state-based behavior in object-oriented analysis and design, as it arises, for example, in specifying behavior in the UML using statecharts. We first provide a rigorous and...
Can Behavioral Requirements be Executed? (And why would we want to do so (2002)
A novel approach to behavioral requirements for reactive systems is described, in which highly expressive scenario-based requirements are \played in" directly from the system's GUI, or...
Multiple Instances and Symbolic Variables in Executable Sequence Charts (2002)
Rami Marelly, David Harel, Hillel Kugler
We extend live sequence charts (LSCs), a highly expressive variant of sequence diagrams, and provide the extension with an executable semantics. The extension involves support for instances that can...
Smart play-out of behavioral requirements (2002)
David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli
submitted for publication. Abstract We describe a methodology for executing scenario-based requirements of reactive sys-tems, focusing on "playing-out " the behavior using formal...
Smart play-out of behavioral requirements (2002)
David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli
submitted for publication. We describe a methodology for executing scenario-based requirements of reactive systems, focusing on “playing-out ” the behavior using formal verification techniques...
Graph drawing by high-dimensional embedding (2002)
We present a novel approach to the aesthetic drawing of undirected graphs. The method has two phases: first embed the graph in a very high dimension and then project it into the 2-D plane using...
Graph drawing by high-dimensional embedding (2002)
Abstract. We present a novel approach to the aesthetic drawing of undirected graphs. The method has two phases: first embed the graph in a very high dimension and then project it into the 2-D plane...
David Harel Sol, David Harel, Sol Efroni, Irun R. Cohen
Software engineers use system visualization mainly in two domains: algorithm visualization and system visualization, and both of these are often animated. In this paper we provide a generic link...
Graph drawing by high-dimensional embedding (2002)
We present a novel approach to the aesthetic drawing of undirected graphs. The method has two phases: first embed the graph in a very high dimension and then project it into the 2-D plane using...
A Fast Multi-scale Method for Drawing Large Graphs (2001)
We present a multi-scale layout algorithm for the aesthetic drawing of undirected graphs with straight-line edges. The algorithm is extremely fast, and is capable of drawing graphs of substantially...
The immune system as a reactive system: Modeling t cell activation with statecharts (2001)
The construction of reliable reactive systems is considered to be one of the most challenging goals in the fields of software and system engineering. The definition of a reactive system suits...
On clustering using random walks (2001)
Abstract. We propose a novel approach to clustering, based on deterministic analysis of random walks on the weighted graph associated with the clustering problem. The method is centered around what...
Modeling biological reactivity: Statecharts vs. boolean logic (2001)
Naaman Kam, David Harel, Irun R. Cohen
Remarkable progress in various fields of biology is leading in the direction of a complete map of the building blocks of biological systems. There is broad agreement among researchers that 21 century...
Modeling languages: Syntax, semantics and all that stuff - part I: The basic stuff (2000)
The motivation for this paper, the rst in a planned series of three parts, is the multitude of concepts surrounding the proper de nition of complex modeling languages for systems and software, and...
Synthesizing State-Based Object Systems from LSC Specifications (2000)
Live sequence charts (LSCs) have been de ned recently as an extension of message sequence charts (MSCs � or their UML variant, sequence diagrams) for rich inter-object speci cation. One of the main...
A Fast Multi-Scale Method for Drawing Large Graphs (2000)
We present a multi-scale layout algorithm for the aesthetic drawing of undirected graphs with straight-line edges. The algorithm is extremely fast, and is capable of drawing graphs that are...
A Fast Multi-Scale Method for Drawing Large Graphs (2000)
We present a multi-scale layout algorithm for the aesthetic drawing of undirected graphs with straight-line edges. The algorithm is extremely fast, and is capable of drawing graphs that are...
An algorithm for blob hierarchy layout (2000)
We present an algorithm for the aesthetic drawing of basic hierarchical blob structures, of the kind found in higraphs and statecharts and in other diagrams in which hierarchy is depicted as...
A Fast Multi-Scale Method for Drawing Large Graphs (2000)
We present a multi-scale layout algorithm for the aesthetic drawing of undirected graphs with straight-line edges. The algorithm is extremely fast, and is capable of drawing graphs that are...
On the Complexity of Verifying Concurrent Transition Systems (2000)
David Harel, Orna Kupferman, Moshe Y. Vardi
In implementation verification, we check that an implementation is correct with respect to a specification by checking whether the behaviors of a transition system that models the program's...
Curriculum and Course Syllabi for a High-School Program in Computer Science (1999)
The authors served on a committee that has designed a high-school curriculum in computer science and supervising the preparation of a comprehensive study program based on it. The new program is...
Curriculum and Course Syllabi for a High-School Program in Computer Science (1999)
The authors served on a committee that designed a high-school curriculum in computer science and has been supervising the preparation of a comprehensive study program based on it. The new program is...
Towards a theory of recursive structures (1998)
harelwisdom.weizmann.ac.il Abstract. In computer science, one is interested mainly in finite ob-jects. Insofar as infinite objects are of interest, they must be computable, i.e., recursive, thus...
Towards a Theory of Recursive Structures (1998)
In computer science, one is interested mainly in finite objects. Insofar as infinite objects are of interest, they must be computable, i.e., recursive, thus admitting an effective finite...
An Algorithm for Straight-Line Drawing of Planar Graphs (1998)
: We present a new algorithm for drawing planar graphs on the plane. It can be viewed as a generalization of the algorithm of Chrobak and Payne, which in turn, is based on an algorithm by de...
LSCs: Breathing Life into Message Sequence Charts (1998)
: While message sequence charts (MSCs) are widely used in industry to document the interworking of processes or objects, they are expressively quite weak, being based on the modest semantic notion of...
LSCs: Breathing Life into Message Sequence Charts (1998)
While message sequence charts (MSCs) are widely used in industry to document the interworking of processes or objects, they are expressively quite weak, being based on the modest semantic notion of a...
Executable Object Modeling with Statecharts (1997)
Abstract: A behaviorally expressive set of diagrammatic languages for modeling object-oriented systems is presented. It constitutes the constructive subset of UML, and is supported by Rhapsody, a...
On the Complexity of Verifying Concurrent Transition Systems (1997)
David Harel, Orna Kupferman, Moshe Y. Vardi
Model-checking methods suffer from the state explosion problem: In a concurrent setting, the program under consideration is typically the parallel composition of many processes, and traversing the...
Computation Paths Logic: An Expressive, yet Elementary, Process Logic (1997)
A new process logic is defined, called computation paths logic (CPL), which treats formulas and programs essentially alike. CPL is a pathwise extension of PDL, following the basic process logic of...
On the Algorithmics of Higraphs (1997)
This paper initiates an algorithmic investigation of higraphs, a formalism proposed in 1988 that combines and extends graphs and Euler/Venn diagrams. We first provide higraphs with a syntax and...
On the Complexity of Verifying Concurrent Transition Systems (1997)
. In implementation verification, we check that an implementation is correct with respect to a specification by checkingwhether the behaviors of a transition system that models the program's...
More on Nonregular PDL: Finite Models and Fibonacci-Like Programs (1996)
: We continue research on enriching propositional dynamic logic (PDL) with nonregular programs. Previous work indicates that the general problem of characterizing those extensions for which PDL...
ACM Trans. Soft. Eng. Method. (1996)
Od Oct, David Harel, Amnon Naamad
We describe the semantics of statecharts as implemented in the Statemate system. This was the first executable semantics defined for the language, and has been in use for almost a decade. In terms of...
More about Recursive Structures: Descriptive Complexity and Zero-One Laws (1996)
: This paper continues our work on infinite, recursive structures. We investigate the descriptive complexity of several logics over recursive structures, including first-order, second-order, and...
Complexity Results for Two-Way and Multi-Pebble Automata and their Logics (1996)
: Two-way and multi-pebble automata are considered (the latter appropriately restricted to accept only regular languages), and enriched with additional features, such as nondeterminism and...
The STATEMATE Semantics of Statecharts (1996)
We describe the semantics of statecharts as implemented in the Statemate system. This was the first executable semantics defined for the language, and has been in use for almost a decade. In terms of...
An Incremental Drawing Algorithm for Planar Graphs (1995)
We present a new algorithm for drawing planar graphs on the plane. It can be viewed as a generalization of the algorithm of Chrobak and Payne, which in turn, is based on an algorithm by de Fraysseix,...
Randomized Graph Drawing with Heavy-Duty Preprocessing (1995)
We present a graph drawing system for general undirected graphs with straight-line edges. It carries out a rather complex set of preprocessing steps, designed to produce a topologically good, but not...
A High-School Program in Computer Science (1995)
Judith Gal-Ezer, Catriel Beeri, David Harel, Amiram Yehudai
The authors are part of a committee that has been designing a new high-school curriculum in computer science and supervising the preparation of a comprehensive study program based on it. The new...
A High-School Program in Computer Science (1995)
Judith Gal-Ezer, Catriel Beeri, David Harel, Amiram Yehudai
The authors are part of a committee that has been designing a new high-school curriculum in computer science and supervising the preparation of a comprehensive study program based on it. The new...
Completeness Results for Recursive Data Bases (1994)
We consider infinite recursive (i.e., computable) relational data bases. Since the set of computable queries on such data bases is not closed under even simple relational operations, one must either...
On the power of bounded concurrency I: Finite automata (1994)
Abstract. We investigate the descriptive succinctness of three fundamental notions for modeling concurrency: nondeterminism and pure parallelism, the two facets of alternation, and bounded...
Deciding emptiness for stack automata on infinite trees (1994)
We show that the emptiness problem for Biichi stack automata on infinite trees is decidable in elementary time. We first establish the decidability of the emptiness problem for pushdown automata on...
Randomized Graph Drawing with Heavy-Duty Preprocessing (1994)
: We present a graph drawing system for general undirected graphs with straight-line edges. It carries out a rather complex set of preprocessing steps, designed to produce a topologically good, but...
Randomized graph drawing with heavy-duty preprocessing (1993)
We present a graph drawing system for general undirected graphs with straight-line edges. It carries out a rather complex set of preprocessing steps, designed to produce a topologically good, but not...
Randomized graph drawing with heavy-duty preprocessing (1993)
We present a graph drawing system for general undirected graphs with straight-line edges. It carries out a rather complex set of preprocessing steps, designed to produce a topologically good, but not...
Randomized graph drawing with heavy-duty preprocessing (1993)
We present a graph drawing system for general undirected graphs with straight-line edges. It carries out a rather complex set of preprocessing steps, designed to produce a topologically good, but not...
Randomized graph drawing with heavy-duty preprocessing (1993)
We present a graph drawing system for general undirected graphs with straight-line edges. It carries out a rather complex set of preprocessing steps, designed to produce a topologically good, but not...
Hamiltonian Paths in Infinite Graphs (1991)
A tight connection is exhibited between infinite paths in recursire trees and HamiltonJan paths in recursire graphs. A corollary is that determining Hamiltonicity in recursire graphs is highly...
92 National Register Bulletin 15: How to Apply the National Register Criteria for Evaluation (1991)
David Harel, Hagi Lachover, Amnon Naamad, Amir Pnueli, Michal Politi, Rivi Sherman, ...
Abstract--This paper provides an overview of the STATEMATE system, constructed over the past several years by the authors and their colleagues at Ad Cad Ltd., the R&D subsidiary of i-Logix, Inc....
Abstract. Elementary translations between various kinds of recursive trees arc prcsented. It is shown that trees of either finite. or countably infinite branching can be effectively put into one-one...
Unger, Ron, Harel, David, Sussman, Joel L.
We present a fast algorithm to produce a graphic matrix representation of sequence homology. The algorithm is based on lexicographical ordering of fragments. It preserves most of the options of a...
David Harel, Dexter Kozen, Jerzy Tiuryn
Dynamic Logic (DL) is a formal system for reasoning about programs. Traditionally, this has meant formalizing correctness specifications and proving rigorously that those specifications are met by a...
North-Holland STATECHARTS: A VISUAL FORMALISM FOR COMPLEX SYSTEMS* (1984)
David Harel, Communicated A. Pnueli
Abstract. We present a broad extension of the conventional formalism of state machines and state diagrams, that is relevant to the specification and design of complex discrete-event systems, such as...
Propositional dynamic logic of nonregular programs (1983)
David Harel, Amir Pnueli, Jonathan Stavi
The borderline between decidable and undecidable propositional dynamic Logic (PDL) is sought when iterative programs represented by regular expressions are augmented with increasingly more complex...
Structure and complexity of relational queries (1982)
This paper is an attempt at laying the foundations for the classification of queries on relational data bases according to their structure and their computational complexity. Using the operations of...
Fox Keller, Evelyn, Harel, David
This paper is a response to the increasing difficulty biologists find in agreeing upon a definition of the gene, and indeed, the increasing disarray in which that concept finds itself. After briefly...
Predicting the Receptive Range of Olfactory Receptors
Haddad, Rafi, Carmel, Liran, Sobel, Noam, Harel, David
Although the family of genes encoding for olfactory receptors was identified more than 15 years ago, the difficulty of functionally expressing these receptors in an heterologous system has, with only...
Explaining a complex living system: dynamics, multi-scaling and emergence
Complex living systems are difficult to understand. They obey the laws of physics and chemistry, but these basic laws do not explain their behaviour; each component part of a complex system...
Using the Statecharts paradigm for simulation of patient flow in surgical care
Boris Sobolev, David Harel, Christos Vasilakis, Adrian Levy
Health care, Hospitals, Surgical services, Patient flow, Simulation, Statecharts,
Prediction Models for the Pleasantness of Binary Mixtures in Olfaction
Lapid, Hadas, Harel, David, Sobel, Noam
Whereas the rules underlying the perceived intensity of binary mixtures have been investigated, minimal efforts have been directed at elucidating the rules underlying the perceived pleasantness of...
Four-dimensional realistic modeling of pancreatic organogenesis
Setty, Yaki, Cohen, Irun R., Dor, Yuval, Harel, David
Organogenesis, the process by which organs develop from individual precursor stem cells, requires that the precursor cells proliferate, differentiate, and aggregate to form a functioning structure....