Search

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

One of the most simple models of computation suitable for representation of reactive systems behavior is a finite state transducer that operates on an input alphabet of control signals and an output alphabet of basic actions. The behavior of such a reactive system displays itself in the correspondence between the flow of control signals and sequence of basic actions performed by the system. We believe that the behavior of this kind requires more complex and expressive means of specifications than the conventional linear temporal logic ($$LTL$$). In this paper, we define a new language of formal specifications $$\mathcal{L}\mathcal{P}$$-$$LTL$$, which is an extension of LTL, specifically intended for describing the properties of transducer computations. In this extension, the temporal operators are parameterized by sets of words (languages) which describe flows of control signals that impact on a reactive system. Basic predicates in the ℒ𝒫-LTL formulas are also defined by the languages in the alphabet of basic actions; these languages describe the expected response of the system to the environmental influences. In our earlier papers, we considered a verification problem for finite state transducers with regard to specifications represented by the ℒ𝒫-$$LTL$$ and ℒ𝒫-$$CTL$$ formulas. It was shown that the problem is algorithmically solvable for both logics. The aim of this paper is to estimate the expressive power of ℒ𝒫-$$LTL$$ by comparing it with some well-known logics widely used in computer science for specification of reactive systems. Two fragments were isolated in the ℒ𝒫-LTL: ℒ𝒫-1-LTL and ℒ𝒫-n-LTL. We discovered that the specification language of ℒ𝒫-1-$$LTL$$ is more expressive than LTL, while the ℒ𝒫-n-$$LTL$$ fragment has the same expressive power as the monadic second order logic S1S. temporal logics, expressive power, specification, verification, Buchi automata, infinite words

Future unmanned aircraft systems are allowed to incorporate operational aspects for flight approval due to the new EASA “specific” category. Incorporating operational aspects offer new possibilities for the verification and validation of complex functions used especially in highly automated vehicles. For these functions, verification and validation can focus on predefined operational aspects prior to flight. In-flight, limits of the operation are monitored to assure the correct working environment for these functions resulting in a safe operation. In this paper, we present the notion of safe operation monitoring and depict operational limits to be supervised. One prominent example for such an operational limit is geofencing. Geofencing prevents an unmanned aircraft from entering a forbidden airspace by using virtual fences. Specifically, in this paper, we present an algorithm and describe parameters for the buffer distance used for the geofence boundary values. The algorithm can be highly parallelized which is important when considering realistic geofences of future operations. Further, we highlight the use of a formal specification language and simulation results which support the verification and validation of geofencing, respectively. The chosen specification language is not limited to geofencing, other operational limits can be expressed and monitored in-flight to assure the safe operation.

A good graphical user interface (GUI) is crucial for an application's usability, so vendors and regulatory agencies increasingly place restrictions on how GUI elements should appear to and interact with users. Motivated by this concern, this paper presents a new technique (based on static analysis) for checking conformance between (Android) applications and GUI policies expressed in a formal specification language. In particular, this paper (1) describes a specification language for formalizing GUI policies, (2) proposes a new program abstraction called an _event-driven layout forest_, and (3) describes a static analysis for constructing this abstraction and checking it against a GUI policy. We have implemented the proposed approach in a tool called Venus, and we evaluate it on 2361 Android applications and 17 policies. Our evaluation shows that Venus can uncover malicious applications that perform ad fraud and identify violations of GUI design guidelines and GDPR laws.

Writing formal specifications often requires users to abstract from the original problem. Especially when verification techniques such as model checking are used. Without applying abstraction the search space the model checker need to traverse tends to grow quickly beyond the scope of what can be checked within reasonable time. The downside of this need to omit details is that it increases the distance to the implementation. Ideally, the created specifications could be used to generate software from (either manually or automatically). But having an incomplete description of the desired system is not enough for this purpose. In this work we introduce the REBEL2 specification language. REBEL2 lets the user write full system specifications in the form of state machines with data without the need to apply abstraction while still preserving the ability to verify non-trivial properties. This is done by allowing the user to _forget_ and _mock_ specifications when running the model checker. The original specifications are untouched by these techniques. We compare the expressiveness of REBEL2 and the effectiveness of _mock_ and _forget_ by implementing two case studies: one from the automotive domain and one from the banking domain. We find that REBEL2 is expressive enough to implement both case studies in a concise manner. Next to that, when performing checks in isolation, mocking can speed up model checking significantly.

Runtime Verification (RV) is a technique to monitor formally-specified properties of the software during its execution. RV has shown to be very effective for bug finding. Unfortunately, RV typically relies on formal specification languages and learning those languages be costly for developers. This paper reports on a study to assess the challenges to specify API properties for the purpose of RV. To that end, we wrote SIESTA, a minimalist specification language, extending Java with two features (the ability to catch calls to specified methods and the ability to access the event history of a given object), and asked inexperienced developers (students) to write specifications in that language for certain parts of the Java API. Among our findings, we observed that 40% of the specifications written by the students matched the ground truth perfectly. The main messages of this work are that 1) it is feasible to use a simple imperative language for specifying properties without significant loss of generality; and that 2) developers are capable of writing specifications in the (programming) language they feel comfortable., This research was partially funded by INES 2.0, FACEPE grants PRONEX APQ 0388-1.03/14, APQ-0399-1.03/17, APQ-0751-1.03/14, and APQ-0570-1.03/14, CAPES grant 88887.136410/2017-00, and CNPq grants 465614/2014-0, 309032/2019-9, 406308/2016-0.

Testing-based formal verification with symbolic execution (TBFV-SE) checks whether programs correctly implement their formal specification. Given a formal specification and a program, it first derives a theorem expressing the correctness property of the executed program paths and then formally verifies the validity of the theorem. However, such theorems still need to be verified manually due to the lack of a tool support for dealing with expressions involved. In this paper, we propose a method for automatically verifying theorems for TBFV-SE. This method uses an SMT solver to check whether a theorem is valid. For this purpose, the method converts the conditions in the theorems written in the SOFL specification language into appropriate constraints that are supported by the SMT solver. We present a tool to support the method, and present two case studies to demonstrate how the tool works in the context of Java programs and SOFL specifications.

Runtime verification allows validation of systems during their operation by monitoring crucial system properties. It is common to generate monitors from temporal specifications formulated in languages like MTL or LTL. However, writing formal specifications might be an obstacle for practitioners. In this paper we present an approach and a tool for generating software monitors for reactive systems from a set of Generalized Test Tables (GTTs)—a table-based, user-friendly specification language specially designed for engineers. The tool is a valuable addition to the already existing static verifier for GTTs since assumptions made in specifications can thus be validated at runtime. Moreover, it makes software and specifications amenable for formal validation that cannot be verified statically. Moreover, the approach is particularly well-suited for the specification of workflows as a collection of tables since it supports dynamic, trigger-based spawning of monitors. The tool produces monitor code in C++ for tables provided in an existing table definition format. We show the usefulness of our approach using characteristic examples.

The domain of Subject-oriented Business Process Management (S-BPM) is somewhat outstanding due to its embracing of Subject Orientation. However, at the same time, it is also a classic BPM domain concerned with typical aspects like creation and exchange of diagrammatic process models, elicitation of domain knowledge, and implementing process (models) into organisations and IT systems. Nevertheless, the Abstract State Machine (ASM) concept, a formal and abstract specification means for algorithms, has been and is fundamental and an important cornerstone for the S-BPM community. The first formal specifications for S-BPM has been developed by Egon Borger using ASM means—namely a specification for an interpreter engine for the subject-oriented modeling language PASS, the Parallel Activity Specification Schema. However, for the sake of intuitive and comprehensive use, ASM can be enriched with defining the passive aspects of PASS, namely the (data) structure of process models and data object appearing in the processes. Here it is useful to complement ASM description means with concepts that are better suited for that tasks. This work analyzes how the S-BPM research community has combined ASM with the Web Ontology Language (OWL) to generate a precise, while comprehensible, system specification for the execution of formal, subject-oriented process models. Furthermore, it will be argued why this combination is worthwhile overcoming the weaknesses of both generic and technology independent specification approaches.

State-based formal specifications benefit from data structuring mechanisms, which collate associated properties and efficiently declare complex types. For example, ‘record’ data structures, similar to those used in programming languages, can be built into the concrete syntax of a language as an enhancement over flat data relationships. While this is relatively simple to achieve for a single-level specification, it becomes significantly more involved when the specification language allows for progressive refinement of the data supporting the specification. Individual fields may be added to create sub-records within a refinement and replaced to create refined records during a refinement step. The impact on the ability to verify invariant and refinement proof obligations must be considered. Here we describe a record structuring syntax that includes notions of extension and inheritance that can be used in a refinement-based formal method. We illustrate the approach using extensions to the Event-B formal method.

Formal verification of real-life industrial software remains a challenging task. It provides strong guarantees of correctness, which are particularly important for security-critical products, such as smart cards. Security of a smart card strongly relies on the requirement that the underlying JavaCard virtual machine ensures necessary isolation properties. This case study paper presents a recent formal verification of a JavaCard Virtual Machine implementation performed by Thales using the Frama-C verification toolset. This is the first verification project for such a large-scale industrial smart card product where deductive verification is applied on the real-life C code. The target properties include common security properties such as integrity and confidentiality. The implementation contains over 7,000 lines of C code. After a formal specification in the ACSL specification language, over 52,000 verification conditions were generated and successfully proved. We present several issues identified during the project, illustrate them by representative examples and present solutions we used to solve them. Finally, we describe proof results, some lessons learned and desired tool improvements.

Describing spatio-temporal behaviors of cyber-physical systems attracts more and more attention in the filed of intelligent transportation systems and biological systems. The major problem is expressiveness and verifiability for modeling and analysis of spatio-temporal behaviors. In order to verify spatial and spatio-temporal behaviors, in this paper, we propose a methodology to model the evolution of spatial scene snapshots and verify the spatio-temporal models. Firstly, we define a novel Topograph through inducing Bigraph in topological space to characterize cyber-physical systems and verify the model against patterns specified with S4u formulas. Secondly, for spatio-temporal verification, we extend Topograph in dense time, named Temporal Topograph, to describe the evolution of spatial objects, which are verified against spatio-temporal specification language. We evaluate the applicability of the approach on CBTC-based intelligent transportation systems.

This paper introduces a deductive verification tool for smart contracts written in Michelson, which is the low-level language of the Tezos blockchain. Our tool accepts a formally specified Michelson contract and automatically translates it to an equivalent program written in WhyML, the programming and specification language of the Why3 framework. Smart contract instructions are mapped into a corresponding WhyML shallow-embedding of the their axiomatic semantics, which we also developed in the context of this work. One major advantage of this approach is that it allows an out-of-the-box integration with the Why3 framework, namely its VCGen and the backend support for several automated theorem provers. We also discuss the use of our tool to automatically prove the correctness of diverse annotated smart contracts.

In autonomous air-traffic management scenarios of the future, manned and unmanned aircraft will be able to safely navigate through the National Airspace System, independent of centralized air-traffic controllers. They will do this by sharing critical data necessary for maintaining standard separation with each other. Under such conditions, every aircraft must have sufficient knowledge about other aircraft sharing the airspace to operate safely. In this paper, we specify a safe state of knowledge that is necessary for aircraft to operate safely in the absence of a centralized air-traffic controller and present a distributed knowledge propagation protocol to attain this safe state. This protocol can be used by network-connected aircraft to achieve collaborative situational awareness for cooperative flight planning. We identify certain system conditions necessary to guarantee two correctness properties for our protocol – safety and progress. We use the TLA + Specification Language to formally specify our protocol, the correctness properties, and the conditions necessary to guarantee the properties. Using the formal specifications, we also provide mechanically-verified proofs of the correctness properties in the TLA + Proof System.

Legal contracts specify the terms and conditions (in essence, requirements) that apply to business transactions. Smart contracts are software systems that monitor and control the execution of contracts to ensure compliance. This paper proposes a formal specification language for contracts, called Symboleo, where contracts consist of collections of obligations and powers that define the legal contract’s compliant executions. The formal semantics of Symboleo is based on an extension of an ontology for Law and is described in terms of logical axioms on statecharts that describe the lifetimes of contracts, obligations and powers. Our proposal includes a preliminary evaluation through the specification of a real life-inspired Sale-of-Goods contract, with a prototype execution engine. We envision this language to enable formally verifying contracts to detect requirements-level issues and to generate executable smart contracts (e.g., on blockchain technology).

Non-fungible tokens are an up and coming application domain for smart contracts. Ethereum is the first blockchain-based decentralized computing platform that has standardized this type of tokens into a well-defined interface, namely ERC721. We propose a framework that provides developers with a smart contract suite that offers complete implementations of the ERC721 standard and common extensions and features frequently encountered in ERC721-based applications. We introduce a specification language that enables efficient customization and configuration of the smart contract suite by including and excluding the supported features and extensions. We evaluate the smart contract suite for its extensibility and reusability and compare the metrics with four other reference implementations tackling a similar problem. In addition to this, we evaluate the effort and efficiency of the specification language and analyze its understandability and learnability in comparison to manual configuration of the smart contract suite. Our contribution lies in examining quality metrics for code extensibility and reusability and determining the more insightful and valuable metrics for assessing these quality attributes in the context of Solidity smart contracts. We also offer a specification language that is a simple and efficient alternative to manually customizing and configuring the smart contract suite by automatically coupling the selected contracts into a deployable final contract.

International audience; The Spatio-Temporal Consistency Language (STeC) is a high-level modeling language that deals natively with spatio-temporal behaviour, i.e., behaviour relating to certain locations and time. Such restriction by both locations and time is of first importance for some types of real-time systems. CCSL is a formal specification language based on logical clocks. It is used to describe some crucial safety properties for real-time systems, due to its powerful expressiveness of logical and chronometric time constraints. We consider a novel verification framework combining STeC and CCSL, with the advantages of addressing spatio-temporal consistency of system behaviour and easily expressing some crucial time constraints. We propose a theory combining these two languages and a method verifying CCSL properties in STeC models. We adopt UPPAAL as the model checking tool and give a simple example to illustrate how to carry out verification in our framework.

As part of the design of a space mission, an important part is the design of so-called flight rules. Flight rules express constraints on various parts and processes of the mission, that if followed, will reduce the risk of failure. One such set of flight rules constrain the format of command sequences regularly (e.g. daily) sent to the spacecraft to control its next near term behavior. We present a high-level view of the automated flight rule checker Frc for checking command sequences sent to NASA’s LADEE Lunar mission spacecraft, used throughout its entire mission. A command sequence is in this case essentially a program (a sequence of commands) with no loops or conditionals, and it can therefore be verified with a trace analysis tool. Frc is implemented using the TraceContract runtime verification tool, an internal Scala DSL for checking event sequences against “formal specifications”. The paper illustrates this untraditional use of runtime verification in a real context, with strong demands on the expressiveness and flexibility of the specification language, illustrating the advantages of an internal DSL.

The autonomous control of unmanned aircraft is a highly safety-critical domain with great economic potential in a wide range of application areas, including logistics, agriculture, civil engineering, and disaster recovery. We report on the development of a dynamic monitoring framework for the DLR ARTIS (Autonomous Rotorcraft Testbed for Intelligent Systems) family of unmanned aircraft based on the formal specification language RTLola. RTLola is a stream-based specification language for real-time properties. An RTLola specification of hazardous situations and system failures is statically analyzed in terms of consistency and resource usage and then automatically translated into an FPGA-based monitor. Our approach leads to highly efficient, parallelized monitors with formal guarantees on the noninterference of the monitor with the normal operation of the autonomous system.

The utilization of a Web services based application depends not only on meeting its functional requirements but also its non-functional requirements. The nonfunctional requirements express the quality of service (QoS) expected from a system. The QoS describes the capability of the service to meet the requirements of its consumers. In the context of Web services, considerations of QoS are critical for a number of reasons. Reliability is among the important QoS requirements of such distributed components as it enhances confidence in the services provided. Although the importance of QoS requirements are well established, they are often ignored until the end of the development cycle. Reasons cited for this are that they are difficult to define and represent precisely, and relay on entities that may not be known at early stages. This articles aims to address the challenges of incorporating the QoS at an early stage of service development and represent it in a precise manner. To achieve this goal, this paper makes use of a process model to facilitate the incorporation of the QoS attributes and Z as the specification language for its formalism. Reliability is used to exemplify the process. The Z schemas have been checked for syntax and type using the Fuzz type checker.

Hands-on tutorials and exercises are recognized as an effective means for gaining much needed cybersecurity and communication and information technology skills. These exercises must be performed in dedicated and virtually isolated computing environments or laboratories, most of which make use of virtualization technology. Building, modifying, and deploying the virtual environments that enable hands-on instruction is currently very time consuming. A new complete exercise instance must be deployed and configured for each course or module, tutorial or exercise, and student. In addition, efficient sharing and reuse of hands-on exercises between organizations is currently extremely difficult, unless the computing resources and virtualization environment are also shared. ADLES is a specification language and associated deployment system created to address these issues up-front. ADLES enables: (1) the formal specification of hands-on virtual computing, networking, and cybersecurity exercises, (2) the automated deployment of specified exercises, and (3) the efficient sharing of such exercises and their computing environment. In this article, we describe in detail the ADLES specification language and deployment system. We also demonstrate ADLES capabilities using two case studies: a pentesting tutorial and a cyber defense competition. The ADLES system is open source and available for all educators to use and improve.

International audience; We summarize several contributions related to the PHP Realistic Annotation and SPEcification Language (Praspel). This language extends PHP programs with annotations for the formal specification of the behavior of their functions and for the declaration of types for their data. These contracts are used to automate test generation, by deriving test cases and test data, and test execution, by checking assertions at run-time in order to establish the test verdict. Our approach to contract-based testing for PHP is fully implemented into a PHP framework currently in use by several web companies.

A Service Workflow is an aggregation of distributed services to fulfill specific functionalities. With ever increasing available services, the methodologies for the selections of the services against the given requirements become main research subjects in multiple disciplines. A few of researchers have contributed to the formal specification languages and the methods for model checking; however, existing methods have the difficulties to tackle with the complexity of workflow compositions. In this paper, we propose to formalize the specification language to reduce the complexity of the workflow composition. To this end, we extend a specification language with the consideration of formal logic, so that some effective theorems can be derived for the verification of syntax, semantics, and inference rules in the workflow composition. The logic-based approach automates compliance checking effectively. The Service Workflow Specification (SWSpec) has been extended and formulated, and the soundness, comple...

With the growing complexity of railway control systems, it is required to preform runtime safety checks of system executions that go beyond conventional runtime monitoring of pre-programmed safety conditions. Runtime verification is a lightweight and rigorous formal method that dynamically analyses execution traces against some formal specifications. A challenge in applying this method in railway systems is defining a suitable monitoring specification language, i.e., a language that is expressive, of reasonable complexity, and easy to understand. In this paper, we propose parameterized modal live sequence charts (PMLSCs) by introducing the alphabet of the specification into charts to distinguish between silent events and unexpected events. We further investigate the expressiveness and complexity theories of the language. In particular, we prove that PMLSCs are closed under negation and the complexity of a subclass of PMLSCs is linear, which allows the language to be used to monitor a system online. Finally, we use PMLSCs to monitor an RBC system in the Chinese high-speed railway and evaluate the performance. The experimental results show that the PMLSC has high monitoring efficiency, and can reduce false alarm rate by introducing alphabets of charts.

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

Object-Z is an object-oriented specification language which extends the Z language with classes, objects, inheritance and polymorphism that can be used to represent the specification of a complex system as collections of objects. There are a number of existing works that mapped Object-Z to C++ and Java programming languages. Since Python and Object-Z share many similarities, both are object-oriented paradigm, support set theory and predicate calculus moreover, Python is a functional programming language which is naturally closer to formal specifications, we propose a mapping from Object-Z specifications to Python code that covers some Object-Z constructs and express its specifications in Python to validate these specifications. The validations are used in the mapping covered preconditions, post-conditions, and invariants that are built using lambda function and Python's decorator. This work has found Python is an excellent language for developing libraries to map Object-Z specifications to Python., Comment: 12 pages, 3 figures

The target of the study is to apply the success of engineering psychology to the area of Formal Engineering Methods, concentrating on validating the requirement specification at system analysis phase of a system development process. This paper presents a systematic approach to integrating specification animation into the process of writing requirements specification. The informal specification animation is used to enhance comprehensible interactions in obtaining feedbacks from the user for the purpose of specification validation, which also improve the current specification. A case study for a travel agent system is used to proof the practicality of the proposed approach. An empirical experiment on the approach is also presented to demonstrate the effectiveness of the approach.

Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The analysis is necessarily an over-approximation as the real executions of the program are not available at analysis time. In contrast, runtime verification techniques have been extensively used for control-oriented properties, analysing the current execution path of the program in a fully automatic manner. In this article, we present a novel approach in which data-oriented and control-oriented properties may be stated in a single formalism amenable to both static and dynamic verification techniques. The specification language we present to achieve this that of ppDATEs, which enhances the control-oriented property language of DATEs, with data- oriented pre/postconditions. For runtime verification of ppDATE specifications, the language is translated into a DATE. We give a formal semantics to ppDATEs, which we use to prove the correctness of our translation from ppDATEs to DATEs. We show how ppDATE specifi- cations can be analysed using a combination of the deductive theorem prover KeY and the runtime verification tool LARVA. Verification is performed in two steps: KeY first partially proves the data-oriented part of the specification, simplifying the specification which is then passed on to LARVA to check at runtime for the remaining parts of the specification including the control-oriented aspects. We show the applicability of our approach on two case studies., peer-reviewed

With the paradigm of aspect-orientation, a developer is able to separate the code of so-called cross-cutting concerns from the rest of the program's logic. This possibility is useful for formal specifications, too. For example, security aspects can be separated from the rest of the specification. Those aspect-oriented specifications often can be more easily reused than extensions that are implemented directly into an existing specification. Another use case is the extension of a specification with new functionality or features. Although this would be possible with refinement too, with aspect-orientation it is not necessary to augment the original specification with “extension points” that can be used for refinement. This paper describes the implementation of the aspect-oriented approach in Abstract State Machines. We introduce an aspect language with its syntax and formal semantics. It allows for specifying pointcuts where an original specification is augmented according to an aspect specification. Besides the general overview of this language extension, some ASM specific features of the realization are depicted in detail. The applicability of aspect-oriented specification in the context of ASM is demonstrated by means of examples, e.g. implementing a fading aspect into the light control system specification of a former ASM case study. Finally, the paper gives a brief overview about the developed tool that supports the writing of aspect-oriented ASMs.

Specifying requirements for complex systems has an important role during software development. At times, the importance of the specification stage gets neglected by software engineers while developing software systems. Software engineering life cycle models are improved for better software quality and reliability. Even though powerful implementation strategies exist, if the requirements of a system to be developed are unclear and not specified properly, then the product can fail to satisfy user needs. Traditional methods use natural language for specifying the requirements of the software systems. The use of formal specifications to specify software systems remains a challenging research problem that needs to be addressed. In this research effort, several healthcare applications that are implemented using Blockchain are studied. Blockchain is a recent invention that uses the idea of decentralization to enforce security. Such applications come with complexity and specifying requirements for such systems using formal specification languages gets even more challenging. The challenges involved in writing formal specifications for such complex applications has been studied in this research effort. The Descartes specification language, a formal executable formal specification language, is used to specify the blockchain healthcare applications under study. Case study examples are used to illustrate the specification of Blockchain healthcare application requirements using the Descartes specification language.

In this era, almost Every person spends 8 to 12 hours in office within a day for the sake of earn money. Offices are considered employees second home as much of the time of employees is spent over there. Employees spent their mental or physical energy to do work in offices and to get money for fulfilments of their desired needs. However, to increase the efficiency and better performance of the employees there are important steps which are followed. The modelling of smart offices provides the system view for understanding and visualizing of office management system from multiple perspectives. In this paper, the modeling and verification of smart office management system is done using UML diagrams, Automata Theory and formal specification language. The operational and behavioral model of the system is captured using UML diagrams. Automata based models are used to provide automated behavior of a system in terms of states. The consistency, accuracy and reliability of the smart office system is done using formal methods. Vienna Development Method and Specification Language (VDM-SL) is used in this paper for verification and validation of the proposed model.

The issue of hotspot occurs when the sink neighboring nodes drain more energy and become dead early. For a time being the whole network is isolated due to dying nodes and the overall lifetime of the network is decreased. Thus, the big challenge in WSANs systems is to prolong the lifetime of the network by solving the Hotspot problem. The lifetime of the network is directly based on the energy consumption of the network. Several challenges are associated with this problem like delays in the network, data packets losses, decrement of lifetime and throughput of the network. Therefore, its need to investigate the issue of Hotspot problem with the help of some energy aware technique. In this paper, the Energy-Aware Distributed Sink Algorithm is introduced to rescue the Hotspot issue in Wireless Sensors and Actors Network (WSANs). The proposed algorithm is formally analyzed with the help of Formal Methods based specification language. For the verification and validation of the proposed algorithm, the Vienna development Method Specification-Language Tool Box (VDM-SL) is used. Both the dynamic and static models are developed to ensure the correctness of the algorithm with some pre/post conditions, invariants, and attributes.

This paper introduces GOSPEL, a behavioral specification language for OCaml. It is designed to enable modular verification of data structures and algorithms. GOSPEL is a contract-based, strongly typed language, with a formal semantics defined by means of translation into Separation Logic. Compared with writing specifications directly in Separation Logic, GOSPEL provides a high-level syntax that greatly improves conciseness and makes it accessible to programmers with no familiarity with Separation Logic. Although GOSPEL has been developed for specifying OCaml code, we believe that many aspects of its design could apply to other programming languages. This paper presents the design and semantics of GOSPEL, and reports on its application for the development of a formally verified library of general-purpose OCaml data structures.

In industrial model-based development (MBD) frameworks, requirements are typically specified informally using textual descriptions. To enable the application of formal methods, these specifications need to be formalized in the input languages of all formal tools that should be applied to analyse the models at different development levels. In this paper we propose a unified approach for the computer-assisted formal specification of requirements and their fully automated translation into the specification languages of different verification tools. We consider a two-stage MBD scenario where first Simulink models are developed from which executable code is generated automatically. We (i) propose a specification language and a prototypical tool for the formal but still textual specification of requirements, (ii) show how these requirements can be translated automatically into the input languages of Simulink Design Verifier for verification of Simulink models and BTC EmbeddedValidator for source code verification, and (iii) show how our unified framework enables besides automated formal verification also the automated generation of test cases.

Security has become an important concern with the development of large scale distributed and heterogeneous multi-agent systems (MAS). One of the main problems in addressing security during the development of MAS is that security is often an afterthought. The cost involved to patch existing systems against vulnerabilities and attacks after deployment is high. If developers and designers can spend some quality time investigating security aspects before beginning to code then this cost can be reduced significantly. Also, using formal methods to specify the complex behavior of large scale software systems has resulted in reliable software systems. This research effort was focused on using formal methods early in the development lifecycle to specify security requirements for MAS. New solutions are emerging to fix security related issues, but how much thought gets in during the early phases of development in terms of security needs to be answered. In this paper, analysis of security requirements for MAS, existing solutions to secure MAS, and the use of formal methods to specify security requirements has been studied. Descartes-Agent, a formal specification language for specifying agent systems has been taken into study to model the security requirements of MAS early on in the development process. Functional specifications of MAS are modelled along with the non-functional security requirements using the Descartes-Agent specification language. This paper also describes the extensions made to the Agent Unified Modeling Language (AUML) to represent the security requirements of MAS. The extensions proposed to AUML are in accordance with the extensions made to the Descartes-Agent specification language. A case study example is used to illustrate the specification of security requirements in MAS using the Descartes-Agent.

Context: Agile software development methods advocate the importance of producing working software without comprehensive documentation. While this approach seems to suit the evolutionary nature of realistic software development for many applications, even including safety-critical systems, it faces two major challenges. One is the lack of a comprehensible specification for code evolution and future maintenance, and the other is the potentially huge cost in code verification. Objective: To address this problem, we believe that supporting the efficient production of system specification by reversing the program constructed as the result of an agile development will be a useful solution. The reverse engineering of specifications from programs will not only help us produce the necessary specification for future program evolution, but more importantly can help us rigorously review the program to detect bugs for the enhancement of program quality. Method: In this paper, we put forward a novel method for rigorously reviewing code by reversing it into a comprehensible, formal specification. We elaborate on the principle of translating code into a specification and discuss how the translation process helps detect bugs in programs. We demonstrate how the proposed method works in practice with examples. We also present an experiment to evaluate the performance of the method by comparing it with existing checklist-based inspection. Conclusions: How to utilize reverse engineering of formal specifications from programs as a means to review the program for bug detection is an almost unexplored topic in software engineering. In this paper, we have described a specific method called RCRRE to reverse engineering of SOFL formal specifications from code and discussed how the reverse engineering process can be taken as an effective means to review the program for bug detection. The principle of converting code to a SOFL specification is reflected by a set of translation patterns and a two-step approach to construct a SOFL specification is established. To evaluate the performance, we have carried out an experiment on the effectiveness of our RCRRE method by comparing it with the CBI approach. The result of the experiment indicates that using our RCRRE method can effectively help the reviewer scrutinize the code and therefore find more bugs than the CBI when the reviewer is rather familiar with the SOFL specification language and skills. In the meanwhile, it also shows that the effectiveness of our RCRRE method may be affected in the situation where the reviewer lacks sufficient understanding and experience of SOFL, and using our RCRRE method may in general take a little longer time than the CBI.

Open standardization seems to be very popular among software developers as it simplifies the standard's adoption by the software engineering. Formal specification methods, while very promising, are being adopted slowly as the industry seems to have little motivation to move into this territory. In this paper the authors present (1) the idea of applying formal specification techniques to open standards' specifications, and (2) an example of a formal specification of the Rich Site Summary (RSS) v2.0 open standard. The authors provide evidence for the advantages of the open standards formal specification over natural language documentations: formal specifications are more concise, less ambiguous, more complete with respect to the original documentation and, when using certain kinds of specification languages, executable and reusable as they support module inheritance. The merging of formal specification methods and open standards allows (1) a more concrete standard design; (2) an improved understanding of the environment under design; (3) an enforced certain level of precision into the specification, and also (4) provides software engineers with extended property checking/verification capabilities, especially if they opt to use any algebraic specification language. The authors showcase how the RSS standard can be formally specified using an algebraic specification language and demonstrate how can that be beneficial.

Component-based software development can help reduce time and cost by means of reusing software components, but the quality of the software may not be ensured if the adopted components contain errors. The Structured Object-oriented Formal Language (SOFL) is a formal specification language that can be used for quality software development. This paper describes a development of desktop application software by connecting with several software components, and how it is developed using SOFL. We introduce how the requirements are analyzed through writing an informal specification and then refining it into a semi-formal specification. We also discuss how the design is carried out by constructing a formal specification in SOFL. Finally, we present the implementation and explain the details of a testing conducted for the quality assurance of the system.

Software design has been well recognized as an important means to achieve high reliability, and formal specification can help enhance the quality of design. However, communications between the designer and the user can become difficult via formal specifications due to the potentially complex mathematical expressions in the specification. This difficulty may lead to the situation where the user may not be closely involved in the process of constructing the specification for quality assurance. To allow formal specification to play more effective roles in software design, we put forward a new approach to deal with this problem in this paper. The approach is characterized by integrating specification animation-based inspection into the process of constructing formal design specifications. We discuss the underlying principle of the approach by explaining how specification animation is utilized as a reading technique for inspection to validate, and then evolve, the current specification towards a satisfactory one. We describe a prototype software tool for the method, and present a case study to show how the method supported by the tool works in practice.

A dynamically reconfigurable system can perform complicated operations with dynamically changing the configuration. For ensuring the safety of the system, a model checking is one of the efficient formal approach. In our work, we define the specification language of a dynamically reconfigurable system and propose the model checking algorithm of verifying safety properties. © 2015 IEEE.

Development of cyber-physical systems include analysis and comprehension of multiple disciplines including mechanical engineering, electronic engineering, systems engineering and computer science. In this research, two consolidated approaches of Model-Based Engineering are used in a combined way for proposing a methodology for requirements analysis, modeling and formal specification of cyber-physical systems. At first, it presents the analysis and classification of the overall system requirements, at high level of abstraction, in order to relate them with the semantics of the MARTE profile. Subsequently, graphical models are presented in the proposed methodology in accordance with formalization of restrictions, annotations and stereotypes through MARTE/VSL. First results of the application of the proposed methodology are presented by means of a case study in the Industrial Packing System domain.

Security has become an important concern with the development of large scale distributed and heterogeneous multi-agent systems (MAS). One of the main problems in addressing security during the development of MAS is that security is often an afterthought. The cost involved to patch existing systems against vulnerabilities and attacks after deployment is high. If developers and designers can spend some quality time investigating security aspects before beginning to code then this cost can be reduced significantly. Also, using formal methods to specify the complex behavior of large scale software systems has resulted in reliable software systems. This research effort was focused on using formal methods early in the development life cycle to specify security requirements for MAS. New solutions are emerging to fix security related issues, but how much thought gets in during the early phases of development in terms of security needs to be answered. In this paper, analysis of security requirements for MAS, existing solutions to secure MAS, and the use of formal methods to specify security requirements has been studied. Descartes - Agent, a formal specification language for specifying agent systems has been taken into study to model the security requirements of MAS early on in the development process. Functional specifications of MAS are modelled along with the non-functional security requirements using the Descartes - Agent specification language. A case study example is used to illustrate the specification of security requirements in MAS using the Descartes - Agent.

In this paper it is presented a software development model based on transformations that allows to derive, in an automatic way, classes in object-oriented programming languages (Ada 95, C++, Eiffel and Java) starting from formal specifications. The set of transformations that conforms the software development model are a systematic steps, which starts from the algebraic specification of a type. This algebraic specification describes the abstract behavior of a type (type of interest) by means of other type, previously specified and implemented (representation type). In a progressive way, the transformations steps allow get a program (class) nearby to the initial specification (type of interest). These transformations obtain -in the first step- an intermediate specification (class specification) that it describes the operations of the type of interest by means of pre and post-conditions. Then, the intermediate specification is used to obtain imperative code in language-independent notation (pseudo-class); and finally the pseudo-class is transformed to any object- oriented programming language for which it has been defined transformations.

AUTOSAR OS is a standard for automotive operating systems, which provides a specification that consists of functionalities such as scheduling services, timing services, and memory protection. In this paper, we focus on memory protection features among them. As the AUTOSAR OS specification is described in natural language, its ambiguity may confuse developers as well as cause the contradiction of the specification, then eventually lead to serious problems of automotive systems such as bugs and errors. These problems in automotive systems relate directly to the safety of human being. Thus, it is very important to ensure the unambiguity and consistency of the specification. Our solution for the problems is formalizing the AUTOSAR OS specification using Event-B specification language which allows us to formally specify the functionalities of AUTOSAR OS and reduce the ambiguity of natural language. We developed a formal specification of the memory protection of AUTOSAR OS and verified its consistency. In this verification, we found the inconsistency of the specification during discharging proof obligations generated by RODIN which is a tool for Event-B. This inconsistency comes from the ambiguity of the original specification, and finding it by reviewing based on natural language description is very hard. In this paper, we explain how we found the inconsistency existed in the AUTOSAR OS standard after showing our approach to formalize and verify it with Event-B.