We present an approach for integration of formal methods within an industrial SW process, illustrating results obtained in a real scenario subject to Military Standard 498 (MIL-STD-498). On the one hand, the formal nucleus of preemptive Time Petri Nets (pTPNs) is used to support design and verification activities of the development process; on the other hand, the Unified Modeling Language (UML) profile for Modeling and Analysis of Real-Time and Embedded (MARTE) systems is adopted to manage the documentation process prescribed by MIL-STD-498. The two cores are integrated by providing guidance for translation of UML-MARTE specifications into equivalent pTPN models, with specific reference to concurrency control and synchronization mechanisms. This permits to attain a smooth transition from the standard artifacts of MIL-STD-498 to pTPN models and analyses, facilitating deployment of the formal core of pTPNs with a limited impact on the industrial practice. The experience proves practical feasibility and effectiveness of the approach, comprising a step towards industrial applicability of formal methods and practices.

Time Petri nets describe the state of a timed system through a marking and a set of clocks. If clocks take values in a dense domain, state space analysis must rely on equivalence classes. These support verification of logical sequencing and quantitative timing of events, but they are hard to be enriched with a stochastic characterization of nondeterminism necessary for performance and dependability evaluation. Casting clocks into a discrete domain overcomes the limitation, but raises a number of problems deriving from the intertwined effects of concurrency and timing. We present a discrete-time variant of time Petri nets, called stochastic preemptive time Petri nets, which provides a unified solution for the above problems through the adoption of a maximal step semantics in which the logical location evolves through the concurrent firing of transition sets. We propose an analysis technique, which integrates the enumeration of a succession relation among sets of timed states with the calculus of their probability distribution. This enables a joint approach to the evaluation of performance and dependability indexes as well as to the verification of sequencing and timeliness correctness. Expressive and analysis capabilities of the model are demonstrated with reference to a real-time digital control system.

A modeling notation is introduced which extends time Petri nets with an additional mechanism of resource assignment making the progress of timed transitions be dependent on the availability of a set of preemptable resources. The resulting notation, which we call preemptive time Petri nets, permits natural description of complex real-time systems running under preemptive scheduling, with periodic, sporadic, and one-shot processes, with nondeterministic execution times, with semaphore synchronizations and precedence relations deriving from internal task sequentialization and from interprocess communication, running on multiple processors. A state space analysis technique is presented which supports the validation of preemptive time Petri net models, combining tight schedulability analysis with exhaustive verification of the correctness of logical sequencing. The analysis technique partitions the state space in equivalence classes in which timing constraints are represented in the form of difference bounds matrixes. This permits it to maintain a polynomial complexity in the representation and derivation of state classes, but it does not tightly encompass the constraints deriving from preemptive behavior, thus producing an enlarged representation of the state space. False behaviors deriving from the approximation can be cleaned-up through an algorithm which provides a necessary and sufficient condition for the feasibility of a behavior along with a tight estimation of its timing profile.

Preemptive Time Petri nets are obtained by extending Time Petri nets with an additional mechanism of resource assignment which makes the progress of timed transitions be dependent on the availability of a set of preemptable resources, and with the capability to make transition times and priorities be dependent on the marking. The combination of these capabilities supports description and verification of flexible real time systems running under preemptive scheduling, with periodic, sporadic and one shot processes, with non-deterministic execution times, with semaphore synchronizations and precedence relations deriving from internal task sequentialization and from interprocess communication. The expressive capabilities of the model and the type of results that can be derived through symbolic enumeration of its dense-timed state space are illustrated with reference to a flexible system mixing dynamic acceptance and performance polymorphism.

A modeling and validation approach extending the formalism of timed Petri nets (TPN) for the analysis of real time systems with flexible scheduling capabilities is introduced. The new formalism is called AdaptiveTPNs. State space analysis of the model supports exhaustive prediction of the time needed to complete critical functions, and permits automatic identification of loading conditions which determine the reduction of the quality of produced results.

A wide increment of object-oriented diffusion has been registered. This is accompanied by the needs of metrics and tools for assessing class reusability, maintainability, complexity, etc. Metrics have to produce confident results and have to be continuously revalidated on the basis of the specific purpose of their adoption. Tools for system assessment must be capable of satisfying the needs of each company by supporting the definition of more specific metrics and by providing appropriate views of software characteristics. These views are useful to give the developers as well as the managers immediately understandable representations of the system status. In this paper a new approach is proposed for system assessment. This approach is based on the adoption of new and well-known metrics together with a set of histograms and profiles that give a clear characterization of the system under development. The semantics of these histograms has been validated against several projects. A brief overview of the tool, TAC++, developed for system assessment is also included.

High level operational languages support the specification and validation of complex reactive systems through the automatic generation of rapid prototypes since the early stages of the development lifecycle. However, when it comes to the implementation stage, these prototypes must be translated into target code to accomplish performance requirements without losing validation results. A transformation method supporting the incremental and automatic transition from rapid prototypes to target code is presented, which relies on a Petri net based specification language. Experimental results are presented to evaluate the performance improvement achieved by this automatic transformation.>

An extended Petri net model which considers modular partitioning along with timing restrictions and environment models is presented. Module constructs permit the specification of a complex system as a set of message passing modules with the timing semantics of time Petri nets. The state space of each individual module can be separately enumerated and assessed under the assumption of a partial specification of the intended module operation environment. State spaces of individual modules can be recursively integrated, to permit the assessment of module clusters and of the overall model, and to check the satisfaction of the assumptions made in the separate analysis of elementary component modules. In the intermediate stages between subsequent integration steps, the state spaces of module and module clusters can be projected onto reduced representations concealing local events that are not essential to the purposes of the analysis. The joint use of incremental enumeration and intermediate concealment of local events allows for a flexible management of state explosion, and permits a scalable approach to the validation of complex systems.

Fiber Distributed Data Interface (FDDI) local area networks (LAN's) are used either as high-speed links between computers and peripherals, or as backbones for lower-speed LAN's, such as Ethernet and Token Ring. The availability of such a high-speed channel will lead to the implementation of high-performance distributed environments spread over a wider area than that allowed by commonly used LAN's. The performance of such distributed environments will strongly depend on that of the interconnecting devices. In this paper, two different algorithms for packet filtering are discussed, referring to bridges interconnecting Ethernet LAN's to FDDI backbones. Algorithm performance is compared with respect to 1) the traffic increase produced on a local Ethernet, and 2) the maximum allowed traffic on remote Ethernets.>

A framework for the development of distributed object-oriented systems in heterogeneous environments is presented. This model attempts to incorporate concepts of distributed computing technology together with software engineering methods. A tool has been developed to enforce the model by means of a high-level specification language and an automatic code generator. However, it is emphasized that the model may be exploited as a methodologic foundation even outside an automatic generation approach.>

The design and implementation of a tool for the construction of distributed systems are described. This tool is based on a specification model which extends ordinary Petri nets to include functional and structural concepts. Functional extensions give the model specification completeness, whereas structuring extensions support the organization of the system under development into a set of message passing modules. The augmented model is named communicating Petri net (CmPN). After an introduction to communicating Petri nets, an outline of the software lifecycle activities enforced by the tool under development is given. Two different methods for automatic code generation are expounded and compared in terms of both computational run-time overhead and code dimension (in the case of an example comprised of four CmPNs).>

Discussed are the most relevant architectural aspects of the the so-called Image Reference Data Base (IRDB), that is the distributed Information System which is under development within the framework of TELEMED Project of the program RACE, project no.R1086, of the Commission of the European Community. The TELEMED Project has the objective of developing a pilot application for experimenting Integrated Broadband Communication of medical, anatomical and radiological information. A major design objective has been the definition of an open system architecture permitting a multisite implememtation of IRDB. To this end, the proposed architecture builds a federation of IRDB and provides a logical view of each individual IRDB as if it were a partition of single database.