Please create an account to participate in the Slashdot moderation system


Forgot your password?
Check out the new SourceForge HTML5 internet speed test! No Flash necessary and runs on all devices. ×

Comment Re:Formal verification is worthless IRL. (Score 1) 531

I love that people can and do undertake this type of thing. It's good for the development and improvement of the state of the art, continued research is valuable purely as research and I don't really want it to stop.

It's also so far removed from pragmatic non-academic reality that it's insane.

SYSGO is a pretty pragmatic non-academic company that has existed in reality since 1991.

Three years, and found two bugs?

Keep in mind that PikeOS was already used in automotive and avionic systems, so it was already rigorously developed and tested. It is indeed quite a testament to the quality of the product.

Let alone the obvious risks around the complexity, completeness and accuracy of a model that took so long to develop.

This model was developed exactly because existing models and theories could not be applied to real-life systems such as the PikeOS microkernel. The papers I linked earlier explicitly discuss managing the complexity.

The EAL link is interesting though, hadn't come across that before.

I hope you are not working on safety-critical systems then.

I suspect most of the systems I work on would qualify at EAL4 but the cost of demonstrating it would kill their commercial value; we'd discontinue the products rather than waste the money.

In the industries where this currently matters, it is the same: you either get your certification (this, or another one depending on the field) or you discontinue the product since you are not allowed to sell it at all (or rather: your prospective customers are not allowed to use it).

EAL7? Comically that's more likely - but only for key algorithms we develop and use. A whole system? Could take down the company..

Another part of the project was about formalising the MILS (multiple independent levels of security) architecture, which enables you to compose components certified at different levels (EAL or otherwise) in a way that does not bring everything down to the level of the least certified component.

And indeed, you will almost never certify an entire system at EAL7.

Comment Re:Formal verification is worthless IRL. (Score 1) 531

constructed a formal model of the PikeOS separation kernel

How long did this take?

The EU project lasted 3 years. Before they could model the kernel, the formal modelling guys had to extend their modelling environment. There were two guys from SYSGO (developers of PikeOS) working (very) part-time on this, two senior researchers from universities, and then some graduate students (I don't think more than two).

Did it actually add any value?

They found 1.5 bugs in PikeOS with it: 1 real bug, and one theoretical bug that could not occur in practice due to the limitations of the API in which it was found (but it was fixed anyway, since you never know whether someone might want to extend it at some point).

Additionally, formal modelling is also a requirement for higher levels of certification, which the PikeOS developers want to reach.

Would it have been quicker to just rewrite PikeOS?

Which language and what development methodology would automatically have the same results as the existing working product and its associated formal model?

Comment Re:Formal verification is worthless IRL. (Score 4, Informative) 531

When you write a program that needs to print the primes up to a certain number, you can easily create a formal proof that your program program is correct.

But when your program is say "apache", that needs to interact with many different browsers on one side, and interpret PHP scripts that interact with databases, this formal proof becomes impossible. Similarly, you cannot write a formal spec for the interaction with the user in for example, a web browser.

While things like the halting problem obviously prevent fully formally proving the correctness of programs, you can go much farther than we generally go today. For example, I participated in an EU project where they constructed a formal model of the PikeOS separation kernel (kind of like an embedded real-time hypervisor). They also generalised this model, which includes support for things like interrupts and context switches.

Comment Re:I'll tell you what could go wrong... (Score 5, Insightful) 144

The general population should just shut their fucking mouths when they feel like spewing an "opinion" about something.

Then why don't you starting by setting a good example?

Science is a process and is hard.

That's why it's perfectly fine for people to voice concerns when they start experimenting in the wild. It's not like we have a perfect overview of how significantly reducing these mosquito populations will affect all other animals that feed on them (and the animals that feed on those, plants that depend on their excrement etc), just to name one potential unintended side effect. Or how it may allow other animals to largely expand their population due to reduced competition for habitats or food sources (mosquitos generally don't survive on blood, that's just what they need for procreation). Or conversely, certain nutrients no longer getting sufficiently removed from the water by mosquito larvae, resulting on too high concentrations of certain substances that then start killing other animals or plants.

TL;DR: Voice educated questions about scientific stuff. Do not broadcast uninformed opinions derived from your safe spot.

If anything is anti-science, it's trying to pre-emptively paint any debate by the general public as uninformed hipster trash. Because that is how you create luddites: by telling people they don't have a say, can't possibly understand anything about the ramifications, and should shut up and defer to some abstract scientists in ivory towers on the authority of some anonymous coward throwing a tantrum.

Comment Re:Seems mostly like a left wing echo chamber (Score 1) 106

Oh, the article obviously very biassed, no question about it. But I like the fact that the author doesn't try to pretend she's not biased or writing in a "balanced" way. It makes it all the more believable to me. But again: it could also be completely made up for all I know, although she's dropping a lot of names of people that were present and specifics that should make it easy to debunk things in that case.

Comment Re: Seems mostly like a left wing echo chamber (Score 2) 106

If the way that Milo guy is portrayed in the article is in any way accurate, he doesn't appear to espouse any viewpoints at all. He just enjoys trolling, including trolling people into believing that what he writes are actually his viewpoints.

Of course Twitter may, like Facebook, help/hurt/hide/quash certain trending topics etc, but I don't think this person's case a particularly good example of how it's ruled by some kind of elite that does not like any dissent.

Comment Re:Well, I _wanted_ to like her. (Score 2) 177

and says that nuclear energy is, "dirty, dangerous and expensive, and should be precluded on all of those counts", when the actual data shows just the opposite.

If you take into account all of the government subsidies, including covering the industry's uninsurable risks, I'm not sure whether at least the cost argument holds.

You forgot that it's the only form of energy that's currently regulated to include all of externalities in its cost.

No, since for nuclear a bunch of externalities are covered by the government at a rate that is below what the market is willing to offer (since the market doesn't want to cover them at all).

For a fair comparison, you'd need to require coal to catch everything (CO2, sulphur, other toxins, more radioactive isotopes than a nuclear plant, etc)
  from all chimneys, transport and store that securely for hundreds of years.

I doubt Jill Stein is very much in favour of coal fired plants.

And despite that, nuclear is still competitive and causes many orders of magnitude less deaths.

Competitive with massive government subsidies, yes. Of course, coal also gets lots of subsidies.

Comment Re:Well, I _wanted_ to like her. (Score 5, Interesting) 177

She's in favor of "homeopathic medicine",

That seems to be a little simplistic, given that she apparently even got the Green Party to remove all mentions of homeopathy from their platform. That said, pure placebo's (such as homeopathy, VR and even the colour of pills) can have their use either separately from (in case of e.g. a hypochondriac) or in combination with regular treatment.

and says that nuclear energy is, "dirty, dangerous and expensive, and should be precluded on all of those counts", when the actual data shows just the opposite.

If you take into account all of the government subsidies, including covering the industry's uninsurable risks, I'm not sure whether at least the cost argument holds.

Furthermore, she wants "a moratorium on GMOs", which wikipedia states, "There is a scientific consensus[147][148][149][150] that currently available food derived from GM crops poses no greater risk to human health than conventional food".

While she indeed argues against it because of safety arguments, there are plenty of other reasons why many people are against GMOs. Just look at the majority of comments on the Slashdot story regarding one of the "GMOs are safe" studies.

I REALLY want to vote third party, but we need some third party candidates who are not anti-science crackpots.

Bashing using arguments that are either easily refuted, or at the very least less clear cut than presented, is anti-science. Name-calling while posting as AC is just silly.

Comment Re:Release the hounds (Score 1) 311

Sounds like a perfect opportunity for a kickstarter to fund legal action against Fox.

If the video owner can catch them for the copyright infringement they can hammer them for Perjury for the DMCA notice.

The problem is that they did not commit perjury regarding the DMCA notice. In the context of a DMCA notice, the only thing that must be true is that you own the copyright to the material you claim that is being infringed. Whether or not the allegedly infringing material actually infringes (and whether you could/should have known this), is irrelevant as far as the DMCA perjury clause is concerned.

It does make me wonder why there haven't been any public DMCA take down campaigns aimed against big companies yet though.

Comment It's not just about Belgium (Score 2) 192

Until now, everyone living within 20km of a nuclear power plant had to have immediate access to iodine pills. The High Council for Health (a scientific body responsible for giving advice concerning health regulations to the government) has advised to increased this radius to 100km, and the government has followed this advice. Everyone in Belgium lives within 100km of a Belgian, Dutch or French nuclear power plant. Hence, iodine pills for everyone.

Comment Re:They are doing the same in Brazil (Score 1) 429

Probably not, but there's plenty of dislike in the US for Brazil's leftwing government, with plenty of attacking propaganda by US political pundits. The last time a coup happen in Brazil it was directly supported by the US. Combine that with the fact that the current president (the one they're trying to impeach) was tortured by US and UK-trained torturers, it's not that far-fetched to assume that some US citizens are also involved in these trolling campaigns (but again, I doubt it's the case for this Igw guy; he's probably just badly informed).

Comment Re:They are doing the same in Brazil (Score 1) 429

Well played, sir troll.

For those not following Brazilian politics, Brazil has been plagued by corruption scandals and economic woes, leading to not a literal coup, but a supermajority vote by the Brazilian House to impeach President Dilma Rousseff, which means it moves to the Senate for confirmation, then an actual trial. It's an emotionally charged issue (some representatives actually burst into song during the impeachment proceedings), but being resolved peacefully.

It's quite a bit more complicated than that.

Slashdot Top Deals

If at first you don't succeed, you must be a programmer.