NDLI: Synthesis from incompatible specifications

Please wait, while we are loading the content...

Wireless innovations for smartphones

Internet-of-energy: combining embedded computing and communication for the smart grid

Debugging embedded multimedia application traces through periodic pattern mining

Finite automata with time-delay blocks

Server-based scheduling of parallel real-time tasks

Trigger memoization in self-triggered control

Shared hardware data structures for hard real-time systems

Code-level timing analysis of embedded software: emsoft'12 invited talk session outline

Estimation of probabilistic bounds on phase CPI and relevance in WCET analysis

An overview of the career of Paul Caspi

Programming parallelism with futures in lustre

On model based synthesis of embedded control software

Mixed critical system design and analysis

Computing without processors

Trends in automotive embedded systems

Smart layers and dumb result: IO characterization of an android-based smartphone

Synthesis from incompatible specifications

Operating system support for redundant multithreading

Feedback thermal control of real-time systems on multicore processors

A low-overhead dedicated execution support for stream applications on shared-memory cmp

Assessing the suitability of the NGMP multi-core processor in the space domain

Towards network-on-chip agreement protocols

A new data flow analysis model for TDM

Runtime verification of real-time embedded systems

A standards-based, fully-open software platform for smart embedded systems

Research issues in smart phones, notepads and related services

XEMU: an efficient QEMU based binary mutation testing framework for embedded software

Timed model checking with abstractions: towards worst-case response time analysis in resource-sharing manycore systems

Flattening hierarchical scheduling

Synthesis of minimal-error control software

Partitioned scheduling for real-time tasks on multiprocessor embedded systems with programmable shared srams

Compositional temporal analysis model for incremental hard real-time system design

Input-output robustness for discrete systems

Synthesis from incompatible specifications

Content Provider	ACM Digital Library
Author	Totla, Nishant Gopi, Sivakanth Radhakrishna, Arjun Černý, Pavol Henzinger, Thomas A.
Abstract	Systems are often specified using multiple requirements on their behavior. In practice, these requirements can be contradictory. The classical approach to specification, verification, and synthesis demands more detailed specifications that resolve any contradictions in the requirements. These detailed specifications are usually large, cumbersome, and hard to maintain or modify. In contrast, quantitative frameworks allow the formalization of the intuitive idea that what is desired is an implementation that comes "closest" to satisfying the mutually incompatible requirements, according to a measure of fit that can be defined by the requirements engineer. One flexible framework for quantifying how "well" an implementation satisfies a specification is offered by simulation distances that are parameterized by an error model. We introduce this framework, study its properties, and provide an algorithmic solution for the following quantitative synthesis question: given two (or more) behavioral requirements specified by possibly incompatible finite-state machines, and an error model, find the finite-state implementation that minimizes the maximal simulation distance to the given requirements. Furthermore, we generalize the framework to handle infinite alphabets (for example, realvalued domains). We also demonstrate how quantitative specifications based on simulation distances might lead to smaller and easier to modify specifications. Finally, we illustrate our approach using case studies on error correcting codes and scheduler synthesis.
Starting Page	53
Ending Page	62
Page Count	10
File Format	PDF
ISBN	9781450314251
DOI	10.1145/2380356.2380371
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2012-10-07
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Synthesis Incompatible specifications
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Synthesis from mixed specifications

Synthesis from production-based specifications

Hardware synthesis from requirement specifications

Generating optimized code from SCR specifications

Efficient gateway synthesis from formal specifications

Reactive synthesis from signal temporal logic specifications

Synthesis of programs from temporal property specifications

Synthesis of hazard-free asynchronous circuits from graphical specifications

Synthesis of optimized hardware transactors from abstract communication specifications

Synthesis from incompatible specifications

Similar Documents

Synthesis from mixed specifications

Synthesis from production-based specifications

Hardware synthesis from requirement specifications

Generating optimized code from SCR specifications

Efficient gateway synthesis from formal specifications

Reactive synthesis from signal temporal logic specifications

Synthesis of programs from temporal property specifications

Synthesis of hazard-free asynchronous circuits from graphical specifications

Synthesis of optimized hardware transactors from abstract communication specifications

Synthesis from incompatible specifications