Search

A formal specification of access control yields a deeper understanding of any operating system, and facilitates performing security analysis of the OS. In this paper, we provide a comprehensive formal specification of access control in Android (ACiA). Prior work is limited in scope, furthermore, recent developments in Android concerning dynamic runtime permissions require rethinking of its formalization. Our formal specification includes three parts, the user-initiated operations (UIOs) and app-initiated operations (AIOs) - which are distinguished based on the initiating entity, and the URI permissions which are utilized in sharing temporary access to data. We also studied the evolution of URI permissions from API 10 (Gingerbread) to API 22 (Lollipop), and a brief discussion on this is included in the paper. Formalizing ACiA allowed us to discover many peculiar behaviors pertaining to ACiA. In addition to that, we discovered two significant issues with permissions in Android which were reported to Google.

In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order) program modules that may incorporate local hidden atoms at different levels. Then, verifying the logic program P amounts to prove some kind of equivalence between P and its modular specification. Under consideration for acceptance in TPLP., Comment: Paper presented at the 36th International Conference on Logic Programming (ICLP 2019), University Of Calabria, Rende (CS), Italy, September 2020, 16 pages

Traditionally, practitioners use formal methods pre-dominately for one half of the quality-assurance process: verification (do we build the software right?). The other half -- validation (do we build the right software?) -- has been given comparatively little attention. While verification is the core of refinement-based formal methods, where each new refinement step must preserve all properties of its abstract model, validation is usually postponed until the latest stages of the development, when models can be automatically executed. Thus mistakes in requirements or in their interpretation are caught too late: usually at the end of the development process. In this paper, we present a novel approach to check compliance between requirements and their formal refinement-based specification during the earlier stages of development. Our proposed approach -- "validation obligations" -- is based on the simple idea that both verification and validation are an integral part of all refinement steps of a system., Comment: ICSE 2021 - NIER

One important way to improve the quality of safety-critical software is to produce a good software requirement satisfying several key properties, such as: integrity, consistency, and well organized, etc. Our work is based on airborne software domain, and propose a framework to translate the software requirements, which are itemized with domain natural language in avionics, effectively into a formal specification model VRM (Variable Relation Model), which has table-style structures with formal semantics. Firstly, considering avionics domain characteristics, a domain concept library is established including different types of variables and concepts. Then, a set of domain-oriented requirements templates are defined, such as: general event/condition, display event/condition, etc. According to VRM model element semantics, three types model construction algorithms are designed to complete the translation automatically. And in the case study, the Engine Indication and Crew Warning System (EICAS) was selected to show how to construct formal models from natural language requirements.

We propose an epistemic approach to formalizing statistical properties of machine learning. Specifically, we introduce a formal model for supervised learning based on a Kripke model where each possible world corresponds to a possible dataset and modal operators are interpreted as transformation and testing on datasets. Then we formalize various notions of the classification performance, robustness, and fairness of statistical classifiers by using our extension of statistical epistemic logic (StatEL). In this formalization, we show relationships among properties of classifiers, and relevance between classification performance and robustness. As far as we know, this is the first work that uses epistemic models and logical formulas to express statistical properties of machine learning, and would be a starting point to develop theories of formal specification of machine learning., Comment: Accepted in Software and Systems Modeling https://rdcu.be/b7ssR This paper is the journal version of the SEFM'19 conference paper arxiv:1907.10327

The lack of systematic approach for product family modeling leads to difficulties in developing a series of high-quality software products simultaneously. This paper tackles this challenge by combining product line approach and formal specification technique. After constructing the feature model of the target family, our approach will start the formalization of the bottom-level features. For each feature, a formal model will be built according to its inner structure and function details. Any problem occurred during this process will cause the evolvement of the feature model under the guidance of a set of pre-defined evolution rules. The final product family model will be established when no problem can be found in both feature model and feature specification. This interleaving of feature model evolvement and feature formalization facilitates consistent and complete product family modeling from both abstract and concrete levels. A case study is given to illustrate the validity of the approach.

Nowadays, protocols often use time to provide better security. For instance, critical credentials are often associated with expiry dates in system designs. However, using time correctly in protocol design is challenging, due to the lack of time related formal specification and verification techniques. Thus, we propose a comprehensive analysis framework to formally specify as well as automatically verify timed security protocols. A parameterized method is introduced in our framework to handle timing parameters whose values cannot be decided in the protocol design stage. In this work, we first propose timed applied $\pi$ -calculus as a formal language for specifying timed security protocols. It supports modeling of continuous time as well as application of cryptographic functions. Then, we define its formal semantics based on timed logic rules , which facilitates efficient verification against various authentication and secrecy properties. Given a parameterized security protocol, our method either produces a constraint on the timing parameters which guarantees the security property satisfied by the protocol, or reports an attack that works for any parameter value. The correctness of our verification algorithm has been formally proved. We evaluate our framework with multiple timed and untimed security protocols and successfully find a previously unknown timing attack in Kerberos V.

Formal specification can benefit software quality by precisely defining the behaviors of operations to prevent primary mistakes in the early phase of software projects, but a remaining challenge is how such a specification can be checked comprehensibly to show whether it satisfies the user’s perception of requirements. In this paper, we describe a new technique for animating operation specifications as a means to address this problem. The technique offers new ways to do (1) automatic animation data generation for both input and output of an operation based on pre- and post-conditions, (2) visualized demonstration of the relationships between input and the corresponding output, (3) comprehensible animation of data items, and (4) illustrative animation of logical expressions and the operators used in them. We discuss these issues and present a prototype tool that supports the automation of the proposed technique. We also report an industrial application as a trial experiment to validate the technique. Finally, we conclude the paper and point out future research directions.

Separation kernels are fundamental software of safety and security-critical systems, which provide their hosted applications with spatial and temporal separation as well as controlled information flows among partitions. The application of separation kernels in critical domain demands the correctness of the kernel by formal verification. To the best of our knowledge, there is no survey paper on this topic. This paper presents an overview of formal specification and verification of separation kernels. We first present the background including the concept of separation kernel and the comparisons among different kernels. Then, we survey the state of the art on this topic since 2000. Finally, we summarize research work by detailed comparison and discussion.

We propose in this paper the Security Policy Language (SePL), which is a formal language for capturing and integrating distributed security policies. The syntax of SePL includes several operators for the integration of policies and it is endowed with a denotational semantics that is a generic semantics, i.e., which is independent of any evaluation environment. We prove the completeness of SePL with respect to sets theory. Furthermore, we provide a formalization of a subset of the eXtensible Access Control Markup Language (XACML), which is the well-known standard informal specification language of Web security policies. We provide also a semantics for XACML policy combining algorithms., Comment: Some major errors in the paper

Robotic systems are becoming more safety critical systems as they are deployed in unstructured human-centered environments. These software intensive systems are composed of distributed, heterogeneous software components interacting in a highly dynamic, uncertain environment. However, no systematic software development process is followed in robotics research. This is a real barrier for system level performance analysis and reasoning, which are in turn required for scalable bench-marking methods and reusing existing software. This chapter provides an end-to-end overview on how robotic software systems can be formally specified from requirement modeling, through solution space exploration, and architecture modeling, and finally to generate executable code. The process is based on SafeRobots framework—a model-driven toolchain for designing software for robotics. Several domain-specific modeling languages that are developed as a part of this integrated approach are also discussed.

The article of record as published may be found at http://link.springer.com/article/10.1007/s11334-016-0286-6 Runtime Monitoring (RM), also known as Runtime Verification (RV), is the process of monitoring and verifying the sequencing and temporal behavior of an underlying application and comparing it to the correct behavior as specified by a formal specification pattern. Hidden Markov Model (HMM)-based RM enables the monitoring of systems with both visible and hidden data, using the same formal specifications used by deterministic RM. This paper describes an online library of formal specification oracles and an accompanying toolset for the runtime monitoring log-files that contain hidden and visible data. Defense Threat Reduction Agency (ID0EIIAC15)

Service-based software (SBS) modeling is considered as a promising way to develop high-quality service-based systems. One major challenge of this methodology is how to effectively utilize existing software services in the process of system modeling to ensure the reliability of the system while reducing the development cost. In this paper, we propose an evolutionary method for the formal specification construction of SBS to tackle this problem. Initial requirements are gradually transformed into a formal design specification through three steps during which existing services are discovered, filtered, selected and adopted. Candidate services are discovered through a keyword-based searching. Then the services are analyzed from both the structural and behavioral perspectives for filtering. A specification-based testing technique is exploited to rigorously determine which candidate services are finally selected. The selected services are incorporated into the formal design model of the system. We present a case study that was conducted for evaluating the usability of the method. We have also developed a prototype tool for supporting the method to be applied in practice.

We formally verify that TCP satisfies its requirements when extended with the Window Scale Option. With the aid of our µCRL specification and the LTSmin toolset, we verify that our specification of unidirectional TCP Data Transfer extended with the Window Scale Option does not deadlock, and that its external behaviour is branching bisimilar to a FIFO queue for a significantly large instance. Separately, we verify that a connection may only be closed if both entities accept the CLOSE call from the Application Layer. Finally, we recommend a rewording of the specification regarding how a zero window is probed, ensuring deadlocks do not arise as a result of misinterpretation. We provide a µCRL specification of TCP extended with the Window Scale Option.Our specification of Data Transfer is branching bisimilar to a FIFO queue.Connection Teardown is verified against requirements expressed in µ-calculus.We recommend a rewording of RFC 793 to avoid deadlocking implementations.

Self-adaptive software systems are able to autonomously adapt their behavior at run-time to react to internal dynamics and to uncertain and changing environment conditions. Formal specification and verification of self-adaptive systems are tasks generally very difficult to carry out, especially when involving time constraints. In this case, in fact, the system correctness depends also on the time associated with events. This article introduces the Zone-based Time Basic Petri nets specification formalism. The formalism adopts timed adaptation models to specify self-adaptive behavior with temporal constraints, and relies on a zone-based modeling approach to support separation of concerns. Zones identified during the modeling phase can be then used as modules either in isolation, to verify intra-zone properties, or all together, to verify inter-zone properties over the entire system. In addition, the framework allows the verification of (timed) robustness properties to guarantee self-healing capabilities when higher levels of reliability and availability are required to the system, especially when dealing with time-critical systems. This article presents also the ZAFETY tool, a Java software implementation of the proposed framework, and the validation and experimental results obtained in modeling and verifying two time-critical self-adaptive systems: the Gas Burner system and the Unmanned Aerial Vehicle system.

This paper presents two computer-aided techniques for discovering formal specification behavioral requirements and for mapping components and methods within an implementation to their driving requirements. The first technique is an informal technique while the second technique is formal. The first technique uses a system reference model abstraction and a set of existing formal specifications to discover implementation components that are not well covered by the formal specification set. This technique also provides a mapping between requirements and code segments driven by those requirements. The second technique uses a bounded constraint solver to match a set of tests with a generic formal specification taken from a small library.

The cost to develop software in aerospace systems is on an exponential curve driven by increasing system complexity, which is exacerbated by a systems engineering process that discovers the majority of design errors late in the design process. Implementing formal specification and analysis techniques starting at the requirements development phase has the potential to drastically reduce aerospace software development costs by identifying and fixing errors while the cost of fault removal is still relatively low. As an example, this paper presents an approach for formalizing common spacecraft attitude control system requirements such as actuator limits, pointing error, reachability, drift, settling time, rise time, and overshoot. The proposed formalization approach allows early analysis of requirements for consistency and can facilitate the generation of rigorous verification evidence from formal methods analysis techniques such as model checking. Limitations in analysis of nonlinear systems by model checking techniques drove use of hypothesis testing as an alternative formal approach for analysis in this research. Formal requirements may be used in hypothesis testing to provide a statistical determination of whether a simulated or tested system meets requirements. To evaluate the use of the formal requirements based hypothesis testing approach, a space filling experimental design simulation is conducted on simulated spacecraft slewing maneuvers. Finally, the results are presented and discussed.

This text is a general, self contained, and tool independent introduction into the Java Modeling Language, JML. It appears in a book about the KeY approach and tool for the verification of Java software, because JML is the dominating starting point of KeY style Java verification. However, this chapter does not depend on any specific tool nor verification methodology in any way. This introduction is written for all readers with an interest in formal specification of software in general, and anyone who wants to learn about the JML approach to specification in particular.

Programming correct parallel software in a cost-effective way is a challenging task requiring a high degree of expertise. As an attempt to overcoming the pitfalls undermining parallel programming, this paper proposes a pattern-based, formally grounded tool that eases writing parallel code by automatically generating platform-dependent programs from high-level, platform-independent specifications. The tool builds on three pillars: (1) a platform-agnostic parallel programming pattern, called PCR, (2) a formal translation of PCRs into a parallel execution model, namely Concurrent Collections (CnC), and (3) a program rewriting engine that generates code for a concrete runtime implementing CnC. The experimental evaluation carried out gives evidence that code produced from PCRs can deliver performance metrics which are comparable with handwritten code but with assured correctness. The technical contribution of this paper is threefold. First, it discusses a parallel programming pattern, called PCR, consisting of producers, consumers, and reducers which operate concurrently on data sets. To favor correctness, the semantics of PCRs is mathematically defined in terms of the formalism FXML. PCRs are shown to be composable and to seamlessly subsume other well-known parallel programming patterns, thus providing a framework for heterogeneous designs. Second, it formally shows how the PCR pattern can be correctly implemented in terms of a more concrete parallel execution model. Third, it proposes a platform-agnostic C++ template library to express PCRs. It presents a prototype source-to-source compilation tool, based on C++ template rewriting, which automatically generates parallel implementations relying on the Intel CnCC++ library. Fil: Perez, Gervasio Daniel. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina Fil: Yovine, Sergio Fabian. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina

The future of Open Distributed Processing systems (ODP) will see an increasing of components number, these components are sharing resources. In general, these resources are offering some kind of services. Due to the huge number of components, it is very difficult to offer the optimum Quality of service (QoS). This encourages us to develop a model for QoS negotiation process to optimize the QoS in an ODP system. In such system, there is a High risk of software or hardware failure. To ensure good performance of a system based on our model, we develop it using a formal method. In our case, we will use Event-B to get in the end of our development a system correct by construction.

The article of record as published may be found at http://dx.doi.org/10.1109/JSYST.2012.2220591 The quality of requirements and the effectiveness of verification and validation (V&V) techniques in guaranteeing that a final system reflects its established requirements have a direct influence on the quality and dependability of the delivered system. The V&V process can be efficient from a managerial point of view, but ineffective from a technical perspective, and vice versa. This paper presents an end-to-end formal computer-aided specification, validation, and verification (SV&V) process, whose feasibility and effectiveness were evaluated against the flight software for the Brazilian Satellite Launcher. Unified modeling language (UML) statechart assertions, scenario-based validation, and runtime verification are used to formally specify and verify the system, and metrics of the ongoing process and its V&V results are collected during the application of the process. The results of the case study indicate that the process and its computer-aided environment were both technically feasible to apply and managerially effective, will likely scale well to cater to SV&V of mission-critical systems that have a larger number of behavioral requirements, and can be used for V&V in a distributed development environment.

This paper presents a diagrammatic logic framework that is suitable for use in formal specification and for reasoning about and refining formal software models. We take a case study style approach to presenting the framework by developing, in some detail, an abstract model for a transparent configuration control platform. The model is built up by stages, corresponding to separate concerns of configuration control. Each successive level is a refinement of the previous level. We discuss the possibilities for developing tools to support the use of the diagrammatic logic, including automated diagram drawing and reasoning procedures. Our wider goal is to make a formal specification easier for its clients to understand.

Formal specification of software components, as a core research area in software engineering, has been widely studied for decades. Although quite a few formal models have been proposed for this purpose, specification of concrete software components is still a challenging task due to the complexity of the functionalities of the components. In this paper, the authors use the stream function model to specify the behavior of priority queue, a commonly used software component. This specification formally defines the regular behavior and fault tolerance behavior of priority queue. In particular, a priority-concatenation operator is defined to handle the ordering of data items to ensure the highest-priority item is removed first. A finite state machine is built based on this specification as an implementation of priority queue. In addition, the authors also discuss a priority upgrading approach to handle possible starvation situation of low-priority data items in the priority queue.

The goal of the research was to check whether we can use a formal specification language such as OCL — Object Constraint Language to express all constraints on the library records proposed by the MARC 21 library standard. The main results are the classification and systematization of the constraints on the structure and the content of the MARC records as well as the specification of the constraints on the data model of MARC 21 in OCL. The obtained results are used in the implementation of the editor for MARC records for validation of the user input. The originality of the work is the adoption of the formal approach in specification of the constraints instead of writing source code in programming language.

The standard hardware design flow involves: (a) design of an integrated circuit using a hardware description language, (b) extensive functional and formal verification, and (c) logical synthesis. However, the above-mentioned processes consume significant effort and time. An alternative approach is to use a formal specification language as a high-level hardware description language and synthesize hardware from formal specifications. Our work is a case study of the synthesis of the widely and industrially used AMBA AHB protocol from formal specifications. Bloem et al. presented the first formal specifications for the AMBA AHB Arbiter and synthesized the AHB Arbiter circuit. However, in the first formal specification some important assumptions were missing. Our contributions are as follows: (a) We present detailed formal specifications for the AHB Arbiter incorporating the missing details, and obtain significant improvements in the synthesis results (both with respect to the number of gates in the synthesized circuit and with respect to the time taken to synthesize the circuit), and (b) we present formal specifications to generate compact circuits for the remaining two main components of AMBA AHB, namely, AHB Master and AHB Slave. Thus with systematic description we are able to automatically and completely synthesize an important and widely used industrial protocol.

We describe the first formal specification of a non-trivial subset of MPI, the dominant communication API in high performance computing. Engineering a formal specification for a non-trivial concurrency API requires the right combination of rigor, executability, and traceability, while also serving as a smooth elaboration of a pre-existing informal specification. It also requires the modularization of reusable specification components to keep the length of the specification in check. Long-lived APIs such as MPI are not usually ‘textbook minimalistic’ because they support a diverse array of applications, a diverse community of users, and have efficient implementations over decades of computing hardware. We choose the TLA+ notation to write our specifications, and describe how we organized the specification of around 200 of the 300 MPI 2.0 functions. We detail a handful of these functions in this paper, and assess our specification with respect to the aforementioned requirements. We close with a description of possible approaches that may help render the act of writing, understanding, and validating the specifications of concurrency APIs much more productive.

A mobile agent system is a special distributed system with moving programs in networks. Mobile agent systems provide a powerful and flexible paradigm for building high performance distributed systems. Due to dynamic configuration property, assuring quality of a mobile agent system is a challenge work. Formal specification and analysis of a mobile agent system provides one of the best approaches to ensure the correctness of a system design. However, it is difficult to find a formal specification tool for modeling a mobile agent system with an easy to understand and concise model. In addition, it is a challenge but also important work to provide an automatic formal analysis approach for verifying whether a system specification correctly meets certain requirements in a mobile agent system. In this paper, a framework for specification and analysis of mobile agent systems is defined. First, Predicate/Transition nets are extended with dynamic channels for modeling mobile agent systems. The formalism has the expressive power to naturally model the software architecture of a mobile agent system, and easily capture the properties especially the mobility, mobile communication and dynamic configuration of a mobile agent system. Then, model checking is instrumented to the framework for automatically verifying the correctness of the specification of a mobile agent system. In order to illustrate the capability of the formalism and the verification strategy, a medical image processing system using mobile agents is modeled using the extended Predicate/Transition nets and system properties are verified using the SPIN model checker.

The formal specification of design patterns is widely recognized as being vital to their effective and correct use in software development. It can clarify the concepts underlying patterns, eliminate ambiguity and thereby lay a solid foundation for tool support. This paper further advances a formal meta-modeling approach that uses first-order predicate logic to specify design patterns. In particular, it specifies both structural and behavioural features of design patterns and systematically captures the variants in a well-structured format. The paper reports a case study involving the formal specification of all 23 patterns in the Gang of Four catalog. It demonstrates that the approach improves the accuracy of pattern specifications by covering variations and clarifying the ambiguous parts of informal descriptions.

Software inspection is a static analysis technique that is widely used for defect detection, but which suffers from a lack of rigor. In this paper, we address this problem by taking advantage of formal specification and analysis to support a systematic and rigorous inspection method. The aim of the method is to use inspection to determine whether every functional scenario defined in the specification is implemented correctly by a set of program paths and whether every program path of the program contributes to the implementation of some functional scenario in the specification. The method is comprised of five steps: deriving functional scenarios from the specification, deriving paths from the program, linking scenarios to paths, analyzing paths against the corresponding scenarios, and producing an inspection report, and allows for a systematic and automatic generation of a checklist for inspection. We present an example to show how the method can be used, and describe an experiment to evaluate its performance by comparing it to perspective-based reading (PBR). The result shows that our method may be more effective in detecting function-related defects than PBR but slightly less effective in detecting implementation-related defects. We also describe a prototype tool to demonstrate the supportability of the method, and draw some conclusions about our work.

This paper presents a formal specification-based software monitoring approach that can dynamically and continuously monitor the behaviors of a target system and explicitly recognize undesirable behaviors in the implementation with respect to its formal specification. The key idea of our approach is in building a monitoring module that connects a specification animator with a program debugger. The requirements information about expected dynamic behaviors of the target system are gathered from the formal specification animator, while the actual behaviors of concrete implementations of the target system are obtained through the program debugger. Based on the information obtained from both sides, the judgement on the conformance of the concrete implementation with respect to the formal specification is made timely while the target system is running. Furthermore, the proposed formal specification-based software monitoring technique does not embed any instrumentation codes to the target system nor does it annotate the target system with any formal specifications. It can detect implementation errors in a real-time manner, and help the developers and users of the system to react to the problems before critical failure occurs.

SUMMARY Model processing programs are regularly used when working with models or synthetizing the code from them; therefore, their verification has become an essential component of constructing reliable software in model-based software engineering. Models are usually formalized and visualized as graphs; therefore, model processing programs based on algebraic graph rewriting systems—such programs are called model transformations—are often applied, and their verification has become an important research area. The goal of our research is to support offline transformation analysis by automated methods, where offline means that only the definition of the program itself, the language definitions of its source and target models are used during the analysis. Therefore, the results are independent from concrete source models, and the analysis needs to be performed only once. Based on previous work, this paper provides the synthesis and of a set of individual components and improves them to provide a complete verification solution: (i) a language is introduced to specify the properties to be verified; (ii) a formalism to describe model transformations in a declarative way; and (iii) automated algorithms that can analyse the declarative transformations as well as the properties expressed by the language. Besides its theoretical basis, the implementation of a verification framework is presented, and its operation is illustrated on a case study. Although the formal verification of model transformation properties is algorithmically undecidable in general, our goal is to provide a practically usable, scoped framework that can largely facilitate the manual verification of model transformations. Copyright © 2013 John Wiley & Sons, Ltd.

Software risk comes mainly from its poor reliability, but how to effectively achieve high reliability still remains a challenge. This paper puts forward a framework for systematically integrating formal specification, review, and testing, and shows how it can be applied to effectively eliminate errors in the major phases of software development process to enhance software reliability. In this framework, requirements errors can be removed and missing requirements can be identified by formalizing requirements into formal specifications whose validity can be ensured by rigorous review. The valid specification can then be used as a firm foundation for implementation and for rigorous inspection, testing, and walkthrough of the implemented program. We discuss how formalization, review, and testing work together at different levels of software development to improve software reliability through detecting and removing errors in documentation.

Because embedded system is combined system of hardware and software, we should design by considering elements such as real-time, reactive, small size, low weight, safe, reliable, harsh environment, low cost, and so on. However, those are poorly reflected on current embedded system development. Especially, there is few existed framework-based embedded system development. As a result, there are many internal codes which is not related with system operation in currently developed embedded system, and reusability or variability is not considered into embedded system development. Therefore we propose a formal specification technique using Z language to guarantee completeness or consistency of design of reusability framework proposed for improving reusability of embedded system. Also we assure correctness of framework design by checking Z model through Z-Eves Tool.

The natural immune system is a subject of great research interests because it provides powerful and flexible information processing capability as a decentralized intelligent system. The immune system constitutes an excellent model of adaptive cooperation at the local level and of emergent behaviour at the global level. These concepts can be applied in the Multi-Agent Systems field where autonomous agents interact in order to solve a common goal. There exists several theories to explain immunological phenomena and software models to simulate various components in the immune system. This paper presents a formal specification of the idiotypic network theory viewed as an agent architecture. The specification gives a precise and non ambiguous description of this architecture which is validated through the automatic generation of traces and interesting properties are proven. This specification constitutes a starting point for understanding, reuse and implementations of this architecture. The approach is illustrated with the robot soccer simulation example.

In this paper an XML based language format to describe specifications of analog IPs and its usage in a validation flow is presented. With the help of an XML-Schema-Definition (XSD) a specification description language called Analog Specification Description in XML (ASDeX) is introduced. An ASDeX-file contains not only specification parameters but also measurement definitions and testbenches to enable specification validation based on simulation. The intention is to generate executable modules (tasks) for running simulations and extracting and checking the actual property values of analog circuits. The task generation is based on a generic template approach using a Meta-Simulator to achieve vendor independent analog IP representation including IP verification.

Manufacturing Execution Systems (MES) optimize production and business processes at the same time. However, the engineering and specification of MES is a challenging, interdisciplinary process. Especially IT and production experts with different views and background have to cooperate. For successful and efficient MES software projects, misunderstandings in the specification process have to be avoided. Therefore, textual specifications need to be complemented by unambiguous graphical models, reducing the complexity by integrating interdisciplinary views and domain specific terms based on different background knowledge. Today's modeling notations focus on the detailed modeling of a certain domain specific problem area. They do not support interdisciplinary discussion adequately. To bridge this gap a novel MES Modeling Language (MES-ML) integrating all necessary views important for MES and pointing out their interdependencies has been developed. Due to its formal basis, comparable and consistent MES-models can be created for specification, standardization, testing, and documentation of MES software. In this paper, the authors present the formal basis of the modeling language and its core notation. The application of MES-ML is demonstrated taking a yogurt production as an example. Finally, the authors give some evaluation results that underline the effectiveness and efficiency of this new modeling approach with reference to four applications in industrial MES-projects in the domain of discrete and hybrid manufacturing., Comment: 10 pages, https://ieeexplore.ieee.org/abstract/document/6145656

Although formal specification techniques are very useful in software development, the acquisition of formal specifications is a difficult task. This paper presents the formal specification language LFC, which is designed to facilitate the acquisition and validation of formal specifications. LFC uses context-free languages for syntactic aspect and relies on a new kind of recursive functions, i.e. recursive functions on context-free languages, for semantic aspect of specifications. Construction and validation of LFC specifications are machine-aided. The basic ideas behind LFC, the main aspects of LFC, and the use of LFC and illustrative examples are described.

Formal specification has proved to be an effective technique for precisely defining software functionality, but validating it against the user's requirements still remains a challenge. In this paper, we propose a novel and practical review approach that utilizes specification animation and trace links to support the reviewing of formal specifications for their validation. The scenario-based animation method dynamically presents the specification to the reviewer by means of "executing" it in a step-by-step manner. It is adopted as a reading technique to guide the reviewer to read the specification and provides him with clear review targets. The trace links that connect the specification to the user's original requirements supply the reviewer with necessary information for determining whether defects are found. We first explain the scenario-based animation and trace links respectively and then propose a group of criteria for validating the formal specification. A case study is described to illustrate the review process at the end of the paper.

This article deals with the problem of dynamic role-playing in Multi-Agent organisations. The approach presented uses a formal specification notation and is based upon a formal framework which defines the concepts of role, interaction and organisation. Within this framework the problem of dynamic role-playing specification is related to the merging of specifications. The formal notation used composes Object-Z and Statecharts. The main features of this approach are: enough expressive power to represent Multi-Agents dynamic aspects, tools for specification analysis and mechanisms allowing the refinement of a high level specification into a low level specification which can be easily implemented. The last part of this paper presents an application with the specification of a reactive and cooperative MAS model named Satisfaction Altruism. An analysis of the specification validates the agents' behaviours.

OpenMP [OpenMP Architecture Review Board. OpenMP application program interface, version 2.5] is an important API for shared memory programming, combining shared memory's potential for performance with a simple programming interface. Unfortunately, OpenMP lacks a critical tool for demonstrating whether programs are correct: a formal memory model. Instead, the current official definition of the OpenMP memory model (the Open-MP 2.5 specification [OpenMP Architecture Review Board. OpenMP application program interface, version 2.5]) is in terms of informal prose. As a result, it is impossible to verify OpenMP applications formally since the prose does not provide a formal consistency model that precisely describes how reads and writes on different threads interact. We expand on our previous work that focused on the formal verification of OpenMP programs through a formal memory model [Greg Bronevetsky and Bronis de Supinski. Formal specification of the memory model. In International Workshop on OpenMP (IWOMP), (2006)]. As in that work, our formalization, which is derived from the existing prose model [OpenMP Architecture Review Board. OpenMP application program interface, version 2.5], provides a two-step process to verify whether an observed OpenMP execution is conformant. This paper extends the model to cover the entire specification. In addition to this formalization, our contributions include a discussion of ambiguities in the current prose-based memory model description. Although our formal model may not capture the current informal memory model perfectly, in part due to these ambiguities, our model reflects our understanding of the informal model's intent. We conclude with several examples that may indicate areas of the OpenMP memory model that need further refinement, however it is specified. Our goal is to motivate the OpenMP community to adopt those refinements eventually, ideally through a formal model, in later OpenMP specifications.

Modeling languages play a cornerstone role in model-driven software development for representing models and metamodels. Modeling languages are usually defined in terms of their abstract and concrete syntax. This allows the rapid development of languages and some associated tools (e.g. editors), but does not allow the representation of their behavioral semantics, something especially important in certain industrial environments in which simulation and verification are critical issues. In this paper we explore the use of Maude as a formal notation for describing models, metamodels, and their dynamic behavior, making models amenable to formal analysis, reasoning, and simulation.

Program slicing is a well-known technique that has been used in a variety of software engineering areas, such as comprehension, understanding, maintenance, debugging, testing, reuse, metrics, etc. This paper discusses how the formal specification language Z schema calculus may be used to specify program slicing. General aspects of program slicing are considered, i.e. dependence graphs and program slicing algorithms. This formalization could help in the correct understanding of program slicing and also the correct application of a desired slicing regime in a rigorous way.

Component-based software engineering (CBSE) is viewed as an opportunity to deal with the increasing complexity of modern-day software. Along with CBSE comes the notion of component markets, where more or less generic pieces of software are traded, to be combined into applications by third-party application developers. For such a component market to work successfully, all relevant properties of components must be precisely and formally described. This is especially true for non-functional properties, such as performance, memory foot print, or security. While the specification of functional properties is well understood, non-functional properties are only beginning to become a research focus. This paper discusses semantic concepts for the specification of non-functional properties, taking into account the specific needs of a component market. Based on these semantic concepts, we present a new specification language QML/CS that can be used to model non-functional product properties of components and component-based software systems.

The development of multiuser and distributed software systems faces the difficulty to program the applications correctly, in a way that guarantees the desired interaction among the users. Motivated by experiences with collaborative t-learning services (i.e. multiuser educational services over Interactive TV), this paper presents a solution to that problem, based on supplementing visual development with formal specification techniques. As a contribution to the development of interactive systems, a software process is introduced that helps defining the separate and the conjoint behavior of different users, incrementally and using highly-accessible formalisms.

Inclusion of Extra-Functional Properties (EFPs) can enrich the quality of component based system design and development. However, such inclusion is a complex engineering task. It is even more complex when reuse possibility of components are high. Formal representation and proper validation mechanism of EFPs can ease the task of inclusion of Extra-functional properties in component based model at design level, subsequent realization at the development level. This paper proposed Z-notation based formal specification of EFPs that facilitates declaration, assignment and evaluation of such EFPs in the context of component-based applications. The proposed approach supported with the validation mechanism of EFPs towards effective design of Component Based Software.

It is difficult to measure the maintainability of a software system early in the development life cycle from its requirement descriptions written in a natural language because informal specifications cannot be analyzed. With the uses of formal description techniques (FDTs) in the communication protocol area since the mid-1980s, avenues have been opened up for a system to be analyzed early in the specification phase. Quantitative measures on its maintainability can then be extracted from such a formal specification, so that we can develop easily maintainable communication software systems and further reduce the increasingly high cost of software maintenance. To date, there is hardly any work done on measuring the maintainability of a system early in its specification phase. This paper presents a method for measuring the maintainability of a communication by using maintainability metrics derived from its formal specification written in Estelle. The methodology for building the Estelle maintainability metrics hierarchy is presented. We have also developed an automated tool, called PSAMS, to automate the calculation of the maintainability indices. We also found that there is a significant correlation between the specification metrics proposed and the widely adopted implementation metrics, thus demonstrating that our proposed metrics are a reliable means of measuring the maintainability of a communication protocol early in the specification phase.

This paper proposes a systematic scheme for synthesizing formal specification from the definitions of relational data model – entity relationship diagram and their data dictionaries. The formal specification of both structural and behavioral properties of relational data model is generated in Z schemas. In our approach, the mandatory structural constraints – the uniqueness of primary key, foreign keys, and referential integrity constraints among the relations in the model, are preserved. We propose a set of transformation rules to produce Z schemas of the states and primitive operations – cascade insertion, deletion, and updating. Moreover, a composition technique of constructing the composite operations is presented by using requirements particle networks. The revision of the formal specification can be easily conducted with the mathematical proofs of the properties of the data model using Z prover tool.