We introduce a typed variant of Safe Ambients, named Secure Safe Ambients (SSA), whose type system allows behavioral invariants of ambients to be expressed and verified. The most significant aspect of the type system is its ability to capture both explicit and implicit process and ambient behavior: process types account not only for immediate behavior, but also for the behavior resulting from capabilities a process acquires during its evolution in a given context. Based on that, the type system provides for static detection of security attacks such as Trojan Horses and other combinations of malicious agents.We study the type system of SSA, define algorithms for type checking and type reconstruction, define languages for expressing security properties, and study a distributed version of SSA and its type system. For the latter, we show that distributed type checking ensures security even in ill-typed contexts, and discuss how it relates to the security architecture of the Java Virtual Machine.
Recently, the importance of dynamic memory management has been increased significantly as there is a growing number of development in object-oriented programs. Many studies show that dynamic memory management is one of the most expensive components in many software systems. It can consume up to 30% of the program execution time. Especially, in C++ programs, it tends to have object creation and deletion prolifically. These objects tend to have short life-spans. This paper describes an integrated study of the C++'s memory allocation behavior, a memory tracing tool and memory managements based on the empirical study of C++ programs. First, this paper summarizes the hypothesis of situations that invoke the dynamic memory management explicitly and implicitly. They are: constructors, copy constructors, overloading assignment operator=, type conversions and application specific member functions. Second, a dynamic memory tracing tool, called mtrace++, is introduced to study the dynamic memory allocation behavior in C++ programs. Third, a dynamic memory allocation strategy, called O-Reuse, to reuse the allocated objects to speed up the object management. At the later part of this paper, an automatic dynamic memory management, called GC++, is discussed. GC++ collects unreferenced objects automatically with high speed of allocation/deallocation processes. The performance gains of O-Reuse and GC++ are come from the utilization of memory allocation/deallocation behavior.
The lexical analyzer of a compiler usually adopts the longest-match rule to resolve ambiguities when deciding the next token in the input stream. However, that rule may not be applicable in all situations. Because the longest-match rule is widely used, a language designer or a compiler implementor frequently overlooks the subtle implications of the rule. The consequence is either a flawed language design or a deficient implementation. We propose a method that automatically checks the applicability of the longest-match rule and identifies precisely the situations in which that rule is not applicable. The method is useful to both language designers and compiler implementors. In particular, the method is indispensable to automatic generators of language translation systems since, without the method, the generated lexical analyzers can only blindly apply the longest-match rule and this results in erroneous behaviors. The crux of the method consists of two algorithms: one is to compute the regular set of the sequences of tokens produced by a nondeterministic Mealy automaton when the automaton processes elements of an input regular set. The other is to determine whether a regular set and a context-free language have nontrivial intersection with a set of equations.
In this paper, we introduce a functional language which facilitates the mobility of code between the sites of a distributed system. We observe that code mobility renders systems with limited resources vulnerable to denial-of-service attacks. Languages which are designed with the objective of preventing these attacks would benefit from static analysis which can expose the resource consumption of programs. In functional computation there is a close connection between the consumption of resources and the flow of control within the system. We show that it is possible to exploit type systems to perform distributed control flow analysis and discuss the potential applications of such analyses in promoting security of resource-sensitive systems.
The single most serious issue in the development of a parallel implementation of non-deterministic programming languages and systems (e.g., logic programming, constraint programming, search-based artificial intelligence systems) is the dynamic management of the binding environments—i.e., the ability to associate with each parallel computation the correct set of bindings/values representing the solution generated by that particular branch of the non-deterministic computation. The problem has been abstracted and formally studied previously (ACM Trans. Program. Lang. Syst. 15(4) (1993) 659; New Generation Comput. 17(3) (1999) 285), but to date only relatively inefficient data structures (ACM Trans. Program. Lang. Syst. (2002); New Generation Comput. 17(3) (1999) 285; J. Funct. Logic Program. Special issue #1 (1999)) have been developed to solve it. We provide a very efficient solution to the problem (O(lgn) per operation). This is a significant improvement over previously best known Ω(n3) solution. Our solution is provably optimal for the pointer machine model. We also show how the solution can be extended to handle the abstraction of search problems in object-oriented systems, with the same time complexity.
In this paper we present ALua, an event-driven communication mechanism for developing distributed parallel applications, based on the interpreted language Lua. We propose a dual programming model for parallel applications, where ALua acts as a gluing element, allowing precompiled program parts to run on different machines. We show, through examples, how three types of applications can benefit from the flexibility that derives from this model. We then present a study of ALua's performance, by comparing execution times of two parallel applications written in ALua with their counterparts written in PVM.
The Ambient Calculus (henceforth, AC) was developed by Cardelli and Gordon as a formal framework to study issues of mobility and migrant code (In: Nivat M, editor. FoSSaCS '98, Lecture Notes in Computer Science, vol. 1378. Berlin: Springer, 1998. p. 140-55). We present a type system for AC that allows the type of exchanged data within the same ambient to vary over time. Our type system assigns what we call behaviors to processes; a denotational semantics of behaviors is proposed, here called trace semantics, underlying much of the remaining analysis. We state and prove a subject reduction property for our typed version of AC. Based on techniques borrowed from finite automata theory, type checking of fully type-annotated processes is shown to be decidable. We show that the typed version of AC originally proposed by Cardelli and Gordon (In: POPL'99, San Antonio, TX. New York: ACM Press, 1999. p. 79-92) can be naturally embedded into our typed version of AC.
The first language computer science students learn, more often than not, is a common production language such as C++ or Java. A minority of curricula, however, begin with a language, such as Scheme, assumed to be a better framework for teaching about computation. SWAY is an experimental teaching language, as expressive as Scheme, but provides an easier transition to production languages. It is a functional language at its core, but adds assignment and a simple object system. One of the goals of SWAY is to incorporate C-style syntax, but to vary from that syntax when pedagogical or ease of programming needs arise. One such area that SWAY differs from languages with C-like expressions is in the selection of items from homogeneous and heterogeneous aggregates. Much like the overloading of the plus operator to add integers as well as reals, a single operator is used for selection in SWAY, regardless of the aggregate structure. It is shown that taking such an approach naturally eases the burden of moving from arrays to objects to lists, in any order, both in teaching and programming.
The three access modifiers-public, protected, and private-control the accessibility of the members of a type in the Java programming language. Furthermore, the accessibility may be transmitted along the two structures-package structure and inheritance structure. It is difficult to identify the weaknesses of the access modifiers from the informal semantics stated in the language manual. We develop a formal framework for specifying the accessibility in Java programs based on attribute grammars. With the help of this framework, we found several situations in the language specification that are irregular or counter-intuitive or ambiguous. These situations may confuse the programmers and hence may create weaknesses in Java programs.
Within this survey article, we explain real-time symbolic timing diagrams and the ICOS tool-box supporting timing-diagram-based requirements capture and rapid prototyping. Real-time symbolic timing diagrams are a full-fledged metric-time temporal logic, but with a graphical syntax reminiscent of the informal timing diagrams widely used in electrical engineering. ICOS integrates a variety of tools, ranging from graphical specification editors over tautology checking and counterexample generation to code generators emitting C or VHDL, thus bridging the gap from formal specification to rapid prototype generation.
Industry is facing a crisis in the design of complex hardware/software systems. Due to the increasing complexity, the gap between the generation of a product idea and the realisation of a working system is expanding rapidly. To manage complexity and to shorten design cycles, industry is forced to look at system-level languages towards specification and design. The (formal) system-level modelling language called POOSL is very expressive and is able to model dynamic hard real-time behaviour and to (visually) capture static (architecture and topology) structure in an object-oriented fashion. The language integrates a process part, based on the process algebra CCS, with a data part, based on the concepts of traditional object-oriented programming languages and it is equipped with a formal semantics. Currently, a number of automated software tools (model editing, simulator and compiler tools) are available in an environment called SHESim. These tools allow visual entry of structure and topology of the system, whereas dynamic behaviour of individual processes is expressed in an expressive imperative language. The formal semantics of POOSL provides a solid basis for the application of verification and performance analysis techniques and establishing a rigorous connection to existing analysis tools.
In this paper we describe languages for formalizing, visualizing and verifying software architectures. This helps us in solving two related problems: (1) the reconstruction of architectures of existing systems, and (2) the definition and verification of architectures of new systems. We define an expression language for formulating architectural rules, a graph language for visualizing various structures of design, and a dialogue language for interactively exercising the former two languages. We have applied these languages in a number of industrial cases.
Wider adoption of formal specification languages in industry is impeded by the lack of support for early development phases and for integration with older, legacy software. Methodology aimed at improving this situation is presented. The methodology uses message sequence charts as a “front-end” specification language and systematically applies an automatic synthesis technique to produce executable specifications in the telecommunications standard Specification and Description Language. Applications of the automatic synthesis technique for both forward and reverse engineering are demonstrated.
Argos belongs to the family of synchronous languages, designed for programming reactive systems: Lustre (Proceedings of the 14th Symposium on Principles of Programming Languages, Munich, 1987; Proc. IEEE 79(9) (1999) 1305), Esterel (Sci. Comput. Programming 19(2) (1992) 87), Signal (Technical Report, IRISA Report 246, IRISA, Rennes, France, 1985). Argos is a set of operators that allow to combine Boolean Mealy machines, in a compositional way. It takes its origin in Statecharts (Sci. Comput. Programming 8 (1987) 231), but with the Argos operators, one can build only a subset of Statecharts, roughly those that do not make use of multi-level arrows. We explain the main motivations for the definition of Argos, and the main differences with Statecharts and their numerous semantics. We define the set of operators, give them a perfectly synchronous semantics in the sense of Esterel, and prove that it is compositional, with respect to the trace equivalence of Boolean Mealy machines. We give an overview of the work related to the definition and implementation of Argos (code generation, connection to verification tools, introduction of non-determinism, etc.). This paper also gives a set of guidelines for building an automaton-based, Statechart-like, yet perfectly synchronous, language.
Graphical representations of business process models are an important means for business architects to grasp the inherent complexity of business processes. This paper reports on the visualisation features of AMBER, the graphical and formal business process language of the Testbed project, and Testbed Studio, its toolkit. Visualisation features fulfill explicit requirements, which are based on an investigation of a business architect's main activities. The paper presents the three main visualisation areas in Testbed: (1) the graphical representation of the language itself, (2) representation conventions, and (3) a set of business process views.
Types in current programming languages specify constant sets of messages always acceptable throughout the lifetime of the types' instances. However, especially in concurrent object-oriented systems, the acceptability of messages often changes with the objects' states. We propose a typed concurrent object calculus where static type checking ensures that users send only acceptable messages although message acceptability may change dynamically. The programmer specifies in types predictable state changes and dependences of message acceptance on states; a compiler infers the needed state information. This state inference has polynomial time complexity and can be used together with subtyping.
This paper presents the distributed implementation of ALIAS, an architecture composed of several cooperating intelligent agents. This system is particularly suited to solve problems in cases where knowledge about the problem domain is incomplete and agents may need to form reasonable hypotheses. In ALIAS agents are equipped with hypothetical reasoning capabilities, performed by means of abduction: if the knowledge available to a logic agent is insufficient to solve a query, the agent could abduce new hypotheses. Each agent is characterized by a local knowledge base represented by an abductive logic program. Agents might differ in their knowledge bases, but must agree on assumed hypotheses. That global knowledge base is dynamically created and managed by means of a shared tuple space. The prototype, developed using Java and Prolog, can run on a TCP/IP network of computers. In the paper, we also discuss some experimental results to evaluate prototype efficiency.
Recent logic programming languages employ dynamic scheduling of calls to improve efficiency of programs. Dynamic scheduling is realized by allowing some calls to be dynamically “delayed” until their arguments are sufficiently instantiated. To this end, logic languages are extended with constructs such as delay declarations. However, many declarative properties that hold for logic and pure Prolog programs do not apply any longer in this extended setting. In particular, the equivalence between the model–theoretic and operational semantics does not hold. In this paper, we study the class of input-consuming programs. Firstly, we argue that input-consuming logic programs are suitable for modeling programs employing delay declarations. Secondly, we show that—under some syntactic restrictions—the S-semantics of a program is correct and fully abstract also for input-consuming programs. This allows us to conclude that for a large class of programs employing delay declarations there exists a model–theoretic semantics which is equivalent to the operational one. Thus, input-consuming programs are shown to be the right answer for conjugate efficiency and declarativeness.
